Remove unnecessary functions and typedefs.

generator/tests/lambda/Lambda.ml

@@ -4,25 +4,25 @@ open LibVar
 
 type coq_val =
 | Coq_val_int  [@f label0] of coq_Z (** Auto Generated Attributes **)
-| Coq_val_clo  [@f label0, label1] of Variables.var * trm (** Auto Generated Attributes **)
+| Coq_val_clo  [@f label0, label1] of var * trm (** Auto Generated Attributes **)
 | Coq_val_err [@f]  (** Auto Generated Attributes **)
 and trm =
 | Coq_trm_val  [@f label0] of coq_val (** Auto Generated Attributes **)
-| Coq_trm_var  [@f label0] of Variables.var (** Auto Generated Attributes **)
-| Coq_trm_abs  [@f label0, label1] of Variables.var * trm (** Auto Generated Attributes **)
+| Coq_trm_var  [@f label0] of var (** Auto Generated Attributes **)
+| Coq_trm_abs  [@f label0, label1] of var * trm (** Auto Generated Attributes **)
 | Coq_trm_app  [@f label0, label1] of trm * trm (** Auto Generated Attributes **)
 | Coq_trm_try  [@f label0, label1] of trm * trm (** Auto Generated Attributes **)
 | Coq_trm_raise  [@f label0] of trm (** Auto Generated Attributes **)
 
-(** val subst : Variables.var -> coq_val -> trm -> trm **)
+(** val subst : var -> coq_val -> trm -> trm **)
 
 let rec subst x v t =
   let s = subst x v in
   (match t with
    | Coq_trm_val v0 -> t
-   | Coq_trm_var y -> if Variables.var_comp x y then Coq_trm_val v else t
+   | Coq_trm_var y -> if var_comp x y then Coq_trm_val v else t
    | Coq_trm_abs (y, t3) ->
-     Coq_trm_abs (y, (if Variables.var_comp x y then t3 else s t3))
+     Coq_trm_abs (y, (if var_comp x y then t3 else 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))
@@ -58,7 +58,7 @@ let if_fault r k =
      | Coq_beh_err -> r)
   | Coq_res_bottom -> r
 
-(** val if_isclo : coq_val -> (Variables.var -> trm -> res) -> res **)
+(** val if_isclo : coq_val -> (var -> trm -> res) -> res **)
 
 let if_isclo v k =
   match v with

generator/tests/lambda/LibFset.ml

-open LibList
-open LibSet
-
-type __ = Obj.t
-let __ = let rec f _ = Obj.repr f in Obj.repr f
-
-module type FsetSig = 
- sig 
-  type 'x fset 
-  
-  val empty : 'a1 fset
-  
-  val singleton : 'a1 -> 'a1 fset
-  
-  val union : 'a1 fset -> 'a1 fset -> 'a1 fset
-  
-  val inter : 'a1 fset -> 'a1 fset -> 'a1 fset
-  
-  val remove : 'a1 fset -> 'a1 fset -> 'a1 fset
-  
-  val from_list : 'a1 list -> 'a1 fset
- end
-
-module FsetImpl = 
- struct 
-  type 'a fset = 'a set
-  
-  (** val build_fset : __ -> 'a1 set **)
-  
-  let build_fset _ =
-    __
-  
-  (** val empty : 'a1 fset **)
-  
-  let empty =
-    build_fset __
-  
-  (** val singleton : 'a1 -> 'a1 set **)
-  
-  let singleton x =
-    build_fset __
-  
-  (** val union : 'a1 fset -> 'a1 fset -> 'a1 set **)
-  
-  let union e f =
-    build_fset __
-  
-  (** val inter : 'a1 fset -> 'a1 fset -> 'a1 set **)
-  
-  let inter e f =
-    build_fset __
-  
-  (** val remove : 'a1 fset -> 'a1 fset -> 'a1 set **)
-  
-  let remove e f =
-    build_fset __
-  
-  (** val from_list : 'a1 list -> 'a1 fset **)
-  
-  let from_list l =
-    fold_right (fun x acc -> union (singleton x) acc) empty l
- end
-

generator/tests/lambda/LibList.ml

-(** val fold_right : ('a1 -> 'a2 -> 'a2) -> 'a2 -> 'a1 list -> 'a2 **)
-
-let rec fold_right f acc l = match l with
-  | [] -> acc
-  | x :: l' -> f x (fold_right f acc l')
-

generator/tests/lambda/LibReflect.ml

-type coq_Decidable =
-  bool
-  (* singleton inductive, whose constructor was decidable_make *)
-
-type 'a coq_Comparable =
-  'a -> 'a -> coq_Decidable
-  (* singleton inductive, whose constructor was make_comparable *)
-

generator/tests/lambda/LibSet.ml

-type __ = Obj.t
-
-type 'a set = __
-

generator/tests/lambda/LibVar.ml

 open Datatypes
-open LibFset
-open LibList
 open LibNat
-open LibReflect
-open Peano
 
-let __ = let rec f _ = Obj.repr f in Obj.repr f
+type var = nat
 
-module type VariablesType = 
- sig 
-  type var 
-  
-  val var_comp : var coq_Comparable
-  
-  val var_comparable : var coq_Comparable
-  
-  type vars = var FsetImpl.fset
-  
-  val var_gen : vars -> var
-  
-  val var_fresh : vars -> var
- end
+(** val var_comp : var coq_Comparable **)
 
-module Variables = 
- struct 
-  type var = nat
-  
-  (** val var_comp : var coq_Comparable **)
-  
-  let var_comp x y =
-    nat_compare x y
-  
-  (** val var_comparable : var coq_Comparable **)
-  
-  let var_comparable =
-    var_comp
-  
-  type vars = var FsetImpl.fset
-  
-  (** val var_gen_list : nat list -> nat **)
-  
-  let var_gen_list l =
-    plus (S O) (fold_right plus O l)
-  
-  (** val var_gen : vars -> var **)
-  
-  let var_gen e =
-    var_gen_list
-      (let s =
-         let h = failwith "AXIOM TO BE REALIZED" in
-         (if h then (fun _ -> true) else (fun _ -> false)) __
-       in
-       if s
-       then failwith "AXIOM TO BE REALIZED"
-       else failwith "AXIOM TO BE REALIZED")
-  
-  (** val var_fresh : vars -> var **)
-  
-  let var_fresh l =
-    var_gen l
- end
+let var_comp x y =
+  nat_compare x y
+
+(** val var_comparable : var coq_Comparable **)
+
+let var_comparable =
+  var_comp
 

generator/tests/lambda/Peano.ml

-open Datatypes
-
-(** val plus : nat -> nat -> nat **)
-
-let rec plus n m =
-  match n with
-  | O -> m
-  | S p -> S (plus p m)
-

generator/tests/lambda/Specif.ml

-type 'a coq_sig =
-  'a
-  (* singleton inductive, whose constructor was exist *)
-