diff --git a/generator/Makefile b/generator/Makefile
index eacba784c7912f71ebf99615e3a31c3fb1391c72..8a29c54a7cd603fc3dbde1d60935c619ddf85fc0 100644
--- a/generator/Makefile
+++ b/generator/Makefile
@@ -42,6 +42,9 @@ tests/%.ml: tests/%.v
 	cd $(<D) && rm *.mli
 	cd $(<D) && $(CURDIR)/../../ml-add-cstr-annots.pl *.ml
 
+tests/lambda/Lambda.ml.d: tests/lambda/Lambda.ml
+	$(OCAMLDEP) -I $(<D) $(<D)/*.ml | $(DEPSED) > $@
+
 tests/%.ml.d: tests/%.ml
 	$(OCAMLDEP) -I $(<D) $< | $(DEPSED) > $@
 
diff --git a/generator/tests/lambda/Lambda.ml b/generator/tests/lambda/Lambda.ml
index 33525dd823993e943a0ce88cd7572a0ad3367052..b00d591c56222836f00b904ef3ca41b6147654fc 100644
--- a/generator/tests/lambda/Lambda.ml
+++ b/generator/tests/lambda/Lambda.ml
@@ -1,9 +1,7 @@
 open BinNums
 open Datatypes
+open LibNat
 open LibVar
-open Specif
-
-let __ = let rec f _ = Obj.repr f in Obj.repr f
 
 type coq_val =
 | Coq_val_int  [@f label0] of coq_Z (** Auto Generated Attributes **)
@@ -24,20 +22,14 @@ let rec subst x v t =
   (match t with
    | Coq_trm_val v0 -> t
    | Coq_trm_var y ->
-     (match let h = failwith "AXIOM TO BE REALIZED" in
-            (match h with
-             | Coq_true -> (fun _ -> Coq_left)
-             | Coq_false -> (fun _ -> Coq_right)) __ with
-      | Coq_left -> Coq_trm_val v
-      | Coq_right -> t)
+     (match nat_compare x y with
+      | Coq_true -> Coq_trm_val v
+      | Coq_false -> t)
    | Coq_trm_abs (y, t3) ->
      Coq_trm_abs (y,
-       (match let h = failwith "AXIOM TO BE REALIZED" in
-              (match h with
-               | Coq_true -> (fun _ -> Coq_left)
-               | Coq_false -> (fun _ -> Coq_right)) __ with
-        | Coq_left -> t3
-        | Coq_right -> s t3))
+       (match nat_compare x y with
+        | Coq_true -> t3
+        | Coq_false -> s t3))
    | Coq_trm_app (t1, t2) -> Coq_trm_app ((s t1), (s t2))
    | Coq_trm_try (t1, t2) -> Coq_trm_try ((s t1), (s t2))
    | Coq_trm_raise t1 -> Coq_trm_raise (s t1))
diff --git a/generator/tests/lambda/Lambda.v b/generator/tests/lambda/Lambda.v
index c29e4f48aca52ff38b146ee41c68eac31cae2ea7..703e41cf3fcae2a461e5d6fcae2536bc07e18bff 100644
--- a/generator/tests/lambda/Lambda.v
+++ b/generator/tests/lambda/Lambda.v
@@ -36,8 +36,8 @@ Fixpoint subst (x:var) (v:val) (t:trm) : trm :=
   let s := subst x v in
   match t with
   | trm_val v => t
-  | trm_var y => If x = y then trm_val v else t
-  | trm_abs y t3 => trm_abs y (If x = y then t3 else s t3)
+  | trm_var y => ifb x = y then trm_val v else t
+  | trm_abs y t3 => trm_abs y (ifb x = y then t3 else s t3)
   | trm_app t1 t2 => trm_app (s t1) (s t2)  
   | trm_try t1 t2 => trm_try (s t1) (s t2) 
   | trm_raise t1 => trm_raise (s t1)
@@ -125,10 +125,14 @@ Fixpoint run (n:nat) (t:trm) : res :=
     end
   end.
 
+Extraction Inline nat_comparable var_comp var_comparable.
 (* As classical logic statements are now unused, they should not be extracted
    (otherwise, useless errors will be launched). *)
 Extraction Inline classicT LibEpsilon.Inhab_witness LibEpsilon.epsilon LibEpsilon.epsilon_def indefinite_description.
 
+(* Suppress dependency on Specif.ml... *)
+Extract Constant var_gen => "failwith ""AXIOM NOT REALISED""".
+
 Set Extraction AccessOpaque.
 Unset Extraction Optimize.
 Unset Extraction KeepSingleton.
diff --git a/generator/tests/lambda/LibNat.ml b/generator/tests/lambda/LibNat.ml
index 20e9a841fe6ff4834f7b42bc353167904b193008..1598c9db946e4183ae4976cd3a33a5ee5099e611 100644
--- a/generator/tests/lambda/LibNat.ml
+++ b/generator/tests/lambda/LibNat.ml
@@ -1,5 +1,4 @@
 open Datatypes
-open LibReflect
 
 (** val nat_compare : nat -> nat -> bool **)
 
@@ -14,8 +13,3 @@ let rec nat_compare x y =
      | O -> Coq_false
      | S y' -> nat_compare x' y')
 
-(** val nat_comparable : nat coq_Comparable **)
-
-let nat_comparable x y =
-  nat_compare x y
-
diff --git a/generator/tests/lambda/LibVar.ml b/generator/tests/lambda/LibVar.ml
index d3286da292edfddf98a392b4d6a1e4ad44a95c7f..ece715d6759cc4b73def3669ee5696814dc5917a 100644
--- a/generator/tests/lambda/LibVar.ml
+++ b/generator/tests/lambda/LibVar.ml
@@ -4,7 +4,6 @@ open LibList
 open LibNat
 open LibReflect
 open Peano
-open Specif
 
 let __ = let rec f _ = Obj.repr f in Obj.repr f
 
@@ -29,13 +28,13 @@ module Variables =
   
   (** val var_comp : var coq_Comparable **)
   
-  let var_comp =
-    nat_comparable
+  let var_comp x y =
+    nat_compare x y
   
   (** val var_comparable : var coq_Comparable **)
   
-  let var_comparable =
-    var_comp
+  let var_comparable x y =
+    nat_compare x y
   
   type vars = var FsetImpl.fset
   
@@ -46,17 +45,7 @@ module Variables =
   
   (** val var_gen : vars -> var **)
   
-  let var_gen e =
-    var_gen_list
-      (let s =
-         let h = failwith "AXIOM TO BE REALIZED" in
-         (match h with
-          | Coq_true -> (fun _ -> Coq_left)
-          | Coq_false -> (fun _ -> Coq_right)) __
-       in
-       match s with
-       | Coq_left -> failwith "AXIOM TO BE REALIZED"
-       | Coq_right -> failwith "AXIOM TO BE REALIZED")
+  let var_gen = failwith "AXIOM NOT REALISED"
   
   (** val var_fresh : vars -> var **)
   
diff --git a/generator/tests/lambda/Specif.ml b/generator/tests/lambda/Specif.ml
index 119dd6308ee4a895c007ead3c5d848ed1f8be0e9..7481ce44d80587a69f75848038e18dbcfa5974a5 100644
--- a/generator/tests/lambda/Specif.ml
+++ b/generator/tests/lambda/Specif.ml
@@ -2,7 +2,3 @@ type 'a coq_sig =
   'a
   (* singleton inductive, whose constructor was exist *)
 
-type sumbool =
-| Coq_left [@f]  (** Auto Generated Attributes **)
-| Coq_right [@f]  (** Auto Generated Attributes **)
-