diff --git a/library/lang/package.scala b/library/lang/package.scala
index c9755e8853b2ea4bd6b01986973557e17da25135..a80e25cbae866b35fc766d300b40ce46701700e0 100644
--- a/library/lang/package.scala
+++ b/library/lang/package.scala
@@ -27,11 +27,6 @@ package object lang {
 
   @ignore
   def error[T](reason: java.lang.String): T = sys.error(reason)
-
-  @ignore
-  implicit class Gives[A](v : A) {
-    def gives[B](tests : A => B) : B = tests(v)
-  }
  
   @ignore
   implicit class Passes[A,B](io : (A,B)) {
diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index 8858fbf3b65f67d4fe51cad9fd52ee020e526129..c8ddeba0a0d269bb672321459b8cee37614a842d 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -111,7 +111,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
         case Hole(_,_) => true
         case _ => false
       }(en)) 
-        e(convertHoles(en, ctx, true))
+        e(convertHoles(en, ctx))
       else
         e(en.toAssert)
     
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index e83f51196a47bfb99570fe4d59bdeeece14f2712..06ab50a2eb19dcf6c8263bd2e647a3e4209ecfca 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -170,28 +170,6 @@ trait ASTExtractors {
         case _ => None
       }
     }
-
-    object ExGives { 
-      def unapply(tree : Apply) : Option[(Tree, List[CaseDef])] = tree match {
-        case Apply(
-          TypeApply(
-            Select(
-              Apply(
-                TypeApply(
-                  ExSelected("leon", "lang", "package", "Gives"),
-                  _ :: Nil
-                ), 
-                body :: Nil
-              ), 
-              ExNamed("gives")
-            ),
-            _ :: Nil
-          ),
-          (Function((_ @ ValDef(_, _, _, EmptyTree)) :: Nil, ExpressionExtractors.ExPatternMatching(_,tests))) :: Nil)
-          => Some((body, tests))
-        case _ => None
-      }
-    }
  
     object ExPasses { 
       def unapply(tree : Apply) : Option[(Tree, Tree, List[CaseDef])] = tree match {
diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala
index 96c3118b52febb9817e9fd75b9bd83ffd185c225..3d9183a7b3deef7c5ff42e6b5f50f443df68a658 100644
--- a/src/main/scala/leon/synthesis/ConvertHoles.scala
+++ b/src/main/scala/leon/synthesis/ConvertHoles.scala
@@ -37,7 +37,7 @@ object ConvertHoles extends LeonPhase[Program, Program] {
    *
    */
 
-  def convertHoles(e : Expr, ctx : LeonContext, treatGives : Boolean = false) : Expr = { 
+  def convertHoles(e : Expr, ctx : LeonContext) : Expr = {
     val (pre, body, post) = breakDownSpecs(e)
 
     // Ensure that holes are not found in pre and/or post conditions