No longer any need for constant extraction of var_gen

generator/tests/lambda/Lambda.v

@@ -130,9 +130,6 @@ Extraction Inline nat_comparable var_comp var_comparable.
    (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.

generator/tests/lambda/LibVar.ml

@@ -4,6 +4,7 @@ open LibList
 open LibNat
 open LibReflect
 open Peano
+open Specif
 
 let __ = let rec f _ = Obj.repr f in Obj.repr f
 
@@ -45,7 +46,17 @@ module Variables =
   
   (** val var_gen : vars -> var **)
   
-  let var_gen = failwith "AXIOM NOT REALISED"
+  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")
   
   (** val var_fresh : vars -> var **)
   

generator/tests/lambda/Specif.ml

@@ -2,3 +2,7 @@ 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 **)
+