diff --git a/src/main/scala/leon/Analysis.scala b/src/main/scala/leon/Analysis.scala
index 2ba7a69ad7aa69be4b49d0cdd7b395dfa2bf6c34..da85f2438743c84c96840e08c24dc06a1d64a284 100644
--- a/src/main/scala/leon/Analysis.scala
+++ b/src/main/scala/leon/Analysis.scala
@@ -328,7 +328,7 @@ object Analysis {
   }
 }
 
-object AnalysisPhase extends plugin.UnitPhase {
+object AnalysisPhase extends UnitPhase {
   val name = "Analysis"
   val description = "Leon Analyses"
 
diff --git a/src/main/scala/leon/ArrayTransformation.scala b/src/main/scala/leon/ArrayTransformation.scala
index 0dab758176b2b3381eaed88c67415d95d5cd8df3..e4ce14c31cc3f6971d971db0b7556a3e7eac02c6 100644
--- a/src/main/scala/leon/ArrayTransformation.scala
+++ b/src/main/scala/leon/ArrayTransformation.scala
@@ -5,7 +5,7 @@ import purescala.Definitions._
 import purescala.Trees._
 import purescala.TypeTrees._
 
-object ArrayTransformation extends plugin.TransformationPhase {
+object ArrayTransformation extends TransformationPhase {
 
   val name = "Array Transformation"
   val description = "Add bound checking for array access and remove array update with side effect"
diff --git a/src/main/scala/leon/EpsilonElimination.scala b/src/main/scala/leon/EpsilonElimination.scala
index 5cc7645d54e99c6480f09dcfd16b46e01e4a0713..e624c47f64c3b636c7282643b6d95bc3b9adb8b3 100644
--- a/src/main/scala/leon/EpsilonElimination.scala
+++ b/src/main/scala/leon/EpsilonElimination.scala
@@ -5,7 +5,7 @@ import purescala.Definitions._
 import purescala.Trees._
 import purescala.TypeTrees._
 
-object EpsilonElimination extends plugin.TransformationPhase {
+object EpsilonElimination extends TransformationPhase {
 
   val name = "Epsilon Elimination"
   val description = "Remove all epsilons from the program"
diff --git a/src/main/scala/leon/FunctionClosure.scala b/src/main/scala/leon/FunctionClosure.scala
index 64c0c123f7d1c289e6b59a0bbe13ddd6390f5ae4..7ce87d90b7b32827a46cd3838391811a7145af93 100644
--- a/src/main/scala/leon/FunctionClosure.scala
+++ b/src/main/scala/leon/FunctionClosure.scala
@@ -5,7 +5,7 @@ import purescala.Definitions._
 import purescala.Trees._
 import purescala.TypeTrees._
 
-object FunctionClosure extends plugin.TransformationPhase{
+object FunctionClosure extends TransformationPhase{
 
   val name = "Function Closure"
   val description = "Closing function with its scoping variables"
diff --git a/src/main/scala/leon/FunctionHoisting.scala b/src/main/scala/leon/FunctionHoisting.scala
index e467f3f20eb0c414936a3584001285fdc24d9eba..813afd9edbf8ea35f9df7f42d6913c13da0fefc7 100644
--- a/src/main/scala/leon/FunctionHoisting.scala
+++ b/src/main/scala/leon/FunctionHoisting.scala
@@ -5,7 +5,7 @@ import purescala.Definitions._
 import purescala.Trees._
 import purescala.TypeTrees._
 
-object FunctionHoisting extends plugin.TransformationPhase {
+object FunctionHoisting extends TransformationPhase {
 
   val name = "Function Hoisting"
   val description = "Hoist function at the top level"
diff --git a/src/main/scala/leon/ImperativeCodeElimination.scala b/src/main/scala/leon/ImperativeCodeElimination.scala
index bb770ba8e15eede296321707f58bcf4460404a98..6f27fc3b494aefffeab9362b0a7fbb1afec5887d 100644
--- a/src/main/scala/leon/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/ImperativeCodeElimination.scala
@@ -5,7 +5,7 @@ import purescala.Definitions._
 import purescala.Trees._
 import purescala.TypeTrees._
 
-object ImperativeCodeElimination extends plugin.TransformationPhase {
+object ImperativeCodeElimination extends TransformationPhase {
 
   val name = "Imperative Code Elimination"
   val description = "Transform imperative constructs into purely functional code"
diff --git a/src/main/scala/leon/plugin/LeonContext.scala b/src/main/scala/leon/LeonContext.scala
similarity index 89%
rename from src/main/scala/leon/plugin/LeonContext.scala
rename to src/main/scala/leon/LeonContext.scala
index 0c6ebabdd2d4eafc77607a8591e3852149038353..584fd333ec9d6a45ecc794252af389471727c5da 100644
--- a/src/main/scala/leon/plugin/LeonContext.scala
+++ b/src/main/scala/leon/LeonContext.scala
@@ -1,5 +1,4 @@
 package leon
-package plugin
 
 import purescala.Definitions.Program
 
diff --git a/src/main/scala/leon/plugin/LeonPhase.scala b/src/main/scala/leon/LeonPhase.scala
similarity index 96%
rename from src/main/scala/leon/plugin/LeonPhase.scala
rename to src/main/scala/leon/LeonPhase.scala
index 13f437ea4b0f1e9eb0846cb6921980320723f62d..1ab05c16fca45a8369d16649fb3ed72196975a83 100644
--- a/src/main/scala/leon/plugin/LeonPhase.scala
+++ b/src/main/scala/leon/LeonPhase.scala
@@ -1,5 +1,4 @@
 package leon
-package plugin
 
 import purescala.Definitions.Program
 
diff --git a/src/main/scala/leon/Simplificator.scala b/src/main/scala/leon/Simplificator.scala
index c9de13922b3a93ee8e9055046dfcf020bd64c74e..6fb6f9ef3078e7d342191d7ddcda654b39cfd3f2 100644
--- a/src/main/scala/leon/Simplificator.scala
+++ b/src/main/scala/leon/Simplificator.scala
@@ -5,7 +5,7 @@ import purescala.Definitions._
 import purescala.Trees._
 import purescala.TypeTrees._
 
-object Simplificator extends plugin.TransformationPhase {
+object Simplificator extends TransformationPhase {
 
   val name = "Simplificator"
   val description = "Some safe and minimal simplification"
diff --git a/src/main/scala/leon/TypeChecking.scala b/src/main/scala/leon/TypeChecking.scala
index 67a2e1bafb7e9d2e9f7f4c169ee77918b45d73d1..d0fd72316b89424d539b3de04c11d90cc4153b82 100644
--- a/src/main/scala/leon/TypeChecking.scala
+++ b/src/main/scala/leon/TypeChecking.scala
@@ -5,7 +5,7 @@ import purescala.Definitions._
 import purescala.Trees._
 import purescala.TypeTrees._
 
-object TypeChecking extends plugin.UnitPhase {
+object TypeChecking extends UnitPhase {
 
   val name = "Type Checking"
   val description = "Type check the AST"
diff --git a/src/main/scala/leon/UnitElimination.scala b/src/main/scala/leon/UnitElimination.scala
index f653b8b7c8d9cd75e1dc60b400410316d1dcb6b3..9604c3a4d3226d26467c826ddc9343cd766e54f3 100644
--- a/src/main/scala/leon/UnitElimination.scala
+++ b/src/main/scala/leon/UnitElimination.scala
@@ -5,7 +5,7 @@ import purescala.Definitions._
 import purescala.Trees._
 import purescala.TypeTrees._
 
-object UnitElimination extends plugin.TransformationPhase {
+object UnitElimination extends TransformationPhase {
 
   val name = "Unit Elimination"
   val description = "Remove all usage of the Unit type and value"
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 5666d15c896210d24a2c48ca64082e96fec5b318..bc9613c4817acd78f4acfed83177b6fe9847ea0d 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -1,10 +1,9 @@
 package leon
 package synthesis
 
-import plugin.LeonContext
 import purescala.Definitions.Program
 
-object SynthesisPhase extends plugin.LeonPhase {
+object SynthesisPhase extends LeonPhase {
   val name        = "Synthesis"
   val description = "Synthesis"