diff --git a/_CoqProject b/_CoqProject
index f0313c5..8aec544 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -40,3 +40,4 @@ theories/SetConstructs.v
 tests/BenchMarks.v
 tests/TestSet.v
 tests/TestMap.v
+tests/TestGenerate.v
diff --git a/src/generate.ml4 b/src/generate.ml4
index 4d39034..603d7be 100644
--- a/src/generate.ml4
+++ b/src/generate.ml4
@@ -2,7 +2,6 @@
 (*i camlp4use: "pa_extend.cmp" i*)
 
 open Format
-open Term
 open EConstr
 open Pp
 open Flags
@@ -50,7 +49,7 @@ let bin_rel_t id_t =
   CAst.make @@ CProdN ([CLocalAssum ([(dl Names.Anonymous);(dl Names.Anonymous)],
 		       Default Decl_kinds.Explicit, mkIdentC id_t)], cprop)
 
-let hole = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None)
+let hole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None)
 
 (* à la v8.2... *)
 let declare_definition
@@ -61,6 +60,13 @@ let declare_definition
   id (loc, false, def_obj_kind) binder_list red_expr_opt constr_expr
   constr_expr_opt decl_hook
 
+let declare_mutual_inductive inds =
+  ComInductive.do_mutual_inductive inds false false false
+    ~uniform:ComInductive.NonUniformParameters Declarations.Finite
+
+let save_transparent_proof () =
+  Lemmas.save_proof (Vernacexpr.Proved (Proof_global.Transparent, None))
+
 (* building the equality predicate *)
 let equiv_ref =
   Libnames.qualid_of_string "Equivalence.equiv"
@@ -231,7 +237,7 @@ let lexi_eqn_constr r carity : branch_expr =
 	  let brlt = dl ([[patc ref_Lt []]], mkIdentC id_Lt) in
 	  let breq = dl ([[patc ref_Eq []]], branch xs ys) in
 	  let brgt = dl ([[patc ref_Gt []]], mkIdentC id_Gt) in
-	  CAst.make @@ CCases (RegularStyle, None, item,
+	  CAst.make @@ CCases (Constr.RegularStyle, None, item,
 			       [brlt; breq; brgt])
       | _, _ -> failwith "Lists should have the same size"
   in
@@ -265,7 +271,7 @@ let make_cmp_def ind mind body =
   let items = [mkIdentC x, None, None;
 	       mkIdentC y, None, None] in
   let branches = branches_constr id_cmp names decls in
-  let body = CAst.make @@ CCases (RegularStyle, None, items, branches) in
+  let body = CAst.make @@ CCases (Constr.RegularStyle, None, items, branches) in
   let def =
     CLambdaN ([CLocalAssum ([dl (Names.Name x); dl (Names.Name y)],
 		Default Decl_kinds.Explicit,
@@ -305,7 +311,7 @@ let prove_refl indconstr mind body =
   let id_t = body.Declarations.mind_typename in
   let id_eq = add_suffix id_t "_eq" in
   let x = Nameops.make_ident "x" None in
-  let ceq = EConstr.of_constr (Universes.constr_of_global
+  let ceq = EConstr.of_constr (UnivGen.constr_of_global
     (Nametab.global (Libnames.qualid_of_ident id_eq))) in
   let goal =
     mkNamedProd x indconstr
@@ -315,15 +321,15 @@ let prove_refl indconstr mind body =
   in
     Lemmas.start_proof (add_suffix id_t "_eq_refl")
       property_kind (get_context goal) goal dummy_hook;
-    ignore(Pfedit.by refltactic);
-    Lemmas.save_proof (Vernacexpr.Proved(Vernacexpr.Transparent,None))
+    ignore (Pfedit.by refltactic);
+    save_transparent_proof ()
 
 let prove_sym indconstr mind body =
   let id_t = body.Declarations.mind_typename in
   let id_eq = add_suffix id_t "_eq" in
   let x = Nameops.make_ident "x" None in
   let y = Nameops.make_ident "y" None in
-  let ceq = EConstr.of_constr (Universes.constr_of_global
+  let ceq = EConstr.of_constr (UnivGen.constr_of_global
     (Nametab.global (Libnames.qualid_of_ident id_eq))) in
   let goal =
     mkNamedProd x indconstr
@@ -336,8 +342,8 @@ let prove_sym indconstr mind body =
   in
     Lemmas.start_proof (add_suffix id_t "_eq_sym")
       property_kind (get_context goal) goal dummy_hook;
-    ignore(Pfedit.by symtactic);
-    Lemmas.save_proof (Vernacexpr.Proved(Vernacexpr.Transparent,None))
+    ignore (Pfedit.by symtactic);
+    save_transparent_proof ()
 
 let prove_trans indconstr mind body =
   let id_t = body.Declarations.mind_typename in
@@ -345,7 +351,7 @@ let prove_trans indconstr mind body =
   let x = Nameops.make_ident "x" None in
   let y = Nameops.make_ident "y" None in
   let z = Nameops.make_ident "z" None in
-  let ceq = EConstr.of_constr (Universes.constr_of_global
+  let ceq = EConstr.of_constr (UnivGen.constr_of_global
     (Nametab.global (Libnames.qualid_of_ident id_eq))) in
   let goal =
     mkNamedProd x indconstr
@@ -362,8 +368,8 @@ let prove_trans indconstr mind body =
   in
     Lemmas.start_proof (add_suffix id_t "_eq_trans")
       property_kind (get_context goal) goal dummy_hook;
-    ignore(Pfedit.by transtactic);
-    Lemmas.save_proof (Vernacexpr.Proved(Vernacexpr.Transparent,None))
+    ignore (Pfedit.by transtactic);
+    save_transparent_proof ()
 
 let prove_Equivalence indconstr mind body =
   prove_refl indconstr mind body;
@@ -392,9 +398,9 @@ let prove_lt_trans indconstr mind body =
   let x = Nameops.make_ident "x" None in
   let y = Nameops.make_ident "y" None in
   let z = Nameops.make_ident "z" None in
-  let clt = EConstr.of_constr (Universes.constr_of_global
+  let clt = EConstr.of_constr (UnivGen.constr_of_global
     (Nametab.global (Libnames.qualid_of_ident id_lt))) in
-  let ceq = EConstr.of_constr (Universes.constr_of_global
+  let ceq = EConstr.of_constr (UnivGen.constr_of_global
     (Nametab.global (Libnames.qualid_of_ident id_eq))) in
   let prove_eq_lt_and_gt () =
     let id_eq_sym = add_suffix id_t "_eq_sym" in
@@ -427,12 +433,12 @@ let prove_lt_trans indconstr mind body =
     in
       Lemmas.start_proof (add_suffix id_t "_eq_lt")
 	lemma_kind (get_context lemma_eq_lt) lemma_eq_lt dummy_hook;
-      ignore(Pfedit.by solve_eq_lt);
-      Lemmas.save_proof (Vernacexpr.Proved(Vernacexpr.Transparent,None));
+      ignore (Pfedit.by solve_eq_lt);
+      save_transparent_proof ();
       Lemmas.start_proof (add_suffix id_t "_eq_gt")
 	lemma_kind (get_context lemma_eq_gt) lemma_eq_gt dummy_hook;
-      ignore(Pfedit.by solve_eq_gt);
-      Lemmas.save_proof (Vernacexpr.Proved(Vernacexpr.Transparent,None))
+      ignore (Pfedit.by solve_eq_gt);
+      save_transparent_proof ()
   in
   let goal =
     mkNamedProd x indconstr
@@ -452,8 +458,8 @@ let prove_lt_trans indconstr mind body =
   prove_eq_lt_and_gt ();
   Lemmas.start_proof (add_suffix id_t "_lt_trans")
     property_kind (get_context goal) goal dummy_hook;
-  ignore(Pfedit.by transtactic);
-  Lemmas.save_proof (Vernacexpr.Proved(Vernacexpr.Transparent,None))
+  ignore (Pfedit.by transtactic);
+  save_transparent_proof ()
 
 let prove_lt_irrefl indconstr mind body =
   let id_t = body.Declarations.mind_typename in
@@ -461,11 +467,11 @@ let prove_lt_irrefl indconstr mind body =
   let id_eq = add_suffix id_t "_eq" in
   let x = Nameops.make_ident "x" None in
   let y = Nameops.make_ident "y" None in
-  let clt = EConstr.of_constr (Universes.constr_of_global
+  let clt = EConstr.of_constr (UnivGen.constr_of_global
     (Nametab.global (Libnames.qualid_of_ident id_lt))) in
-  let ceq = EConstr.of_constr (Universes.constr_of_global
+  let ceq = EConstr.of_constr (UnivGen.constr_of_global
     (Nametab.global (Libnames.qualid_of_ident id_eq))) in
-  let cfalse = EConstr.of_constr (Universes.constr_of_global
+  let cfalse = EConstr.of_constr (UnivGen.constr_of_global
     (Nametab.global (Libnames.qualid_of_ident (Names.Id.of_string "False")))) in
   let goal =
     mkNamedProd x indconstr
@@ -481,8 +487,8 @@ let prove_lt_irrefl indconstr mind body =
   in
     Lemmas.start_proof (add_suffix id_t "_lt_irrefl")
       property_kind (get_context goal) goal dummy_hook;
-    ignore(Pfedit.by irrefltactic);
-    Lemmas.save_proof (Vernacexpr.Proved(Vernacexpr.Transparent,None))
+    ignore (Pfedit.by irrefltactic);
+    save_transparent_proof ()
 
 let build_strictorder_ref =
   Libnames.qualid_of_string "Containers.OrderedType.Build_StrictOrder"
@@ -511,13 +517,13 @@ let prove_t_compare_spec indconstr mind body =
   let id_cmp = add_suffix id_t "_cmp" in
   let x = Nameops.make_ident "x" None in
   let y = Nameops.make_ident "y" None in
-  let clt = EConstr.of_constr (Universes.constr_of_global
+  let clt = EConstr.of_constr (UnivGen.constr_of_global
     (Nametab.global (Libnames.qualid_of_ident id_lt))) in
-  let ceq = EConstr.of_constr (Universes.constr_of_global
+  let ceq = EConstr.of_constr (UnivGen.constr_of_global
     (Nametab.global (Libnames.qualid_of_ident id_eq))) in
-  let ccmp = EConstr.of_constr (Universes.constr_of_global
+  let ccmp = EConstr.of_constr (UnivGen.constr_of_global
     (Nametab.global (Libnames.qualid_of_ident id_cmp))) in
-  let ccomp_spec = EConstr.of_constr (Universes.constr_of_global
+  let ccomp_spec = EConstr.of_constr (UnivGen.constr_of_global
     (Nametab.global (Libnames.qualid_of_ident
 		       (Names.Id.of_string "compare_spec")))) in
   let goal =
@@ -531,8 +537,8 @@ let prove_t_compare_spec indconstr mind body =
   in
   Lemmas.start_proof (add_suffix id_t "_compare_spec")
     property_kind (get_context goal) goal dummy_hook;
-  ignore(Pfedit.by spectactic);
-  Lemmas.save_proof (Vernacexpr.Proved(Vernacexpr.Transparent,None))
+  ignore (Pfedit.by spectactic);
+  save_transparent_proof ()
 
 let build_ot_ref =
   Libnames.qualid_of_string "Containers.OrderedType.Build_OrderedType"
@@ -562,7 +568,7 @@ let prove_OrderedType indconstr mind body =
 
 let generate_simple_ot gref =
   let gindref = Nametab.global gref in
-  let indconstr = Universes.constr_of_global gindref in
+  let indconstr = UnivGen.constr_of_global gindref in
   let indeconstr = EConstr.of_constr indconstr in
   (* retrieve the inductive type *)
   let (ind, ctx) =
@@ -572,11 +578,11 @@ let generate_simple_ot gref =
   (* define the equality predicate *)
   let mutual_eq = make_eq_mutual ind mind ibody in
   (* fprintf std_formatter "%a" print_inductive_def mutual_eq; *)
-  ComInductive.do_mutual_inductive mutual_eq false false false ComInductive.NonUniformParameters Declarations.Finite;
+  declare_mutual_inductive mutual_eq;
   (* define the strict ordering predicate *)
   let mutual_lt = make_lt_mutual ind mind ibody in
   (* fprintf std_formatter "%a" print_inductive_def mutual_lt; *)
-  ComInductive.do_mutual_inductive mutual_lt false false false ComInductive.NonUniformParameters Declarations.Finite;
+  declare_mutual_inductive mutual_lt;
   (* declare the comparison function *)
   let id_cmp, ttt = make_cmp_def ind mind ibody in
     declare_definition id_cmp
@@ -732,7 +738,7 @@ let rlexi_eqn_constr r cmpid carity cmask =
 	 let brlt = dl ([[patc ref_Lt []]], mkIdentC id_Lt) in
 	 let breq = dl ([[patc ref_Eq []]], branch xs ys masks) in
 	 let brgt = dl ([[patc ref_Gt []]], mkIdentC id_Gt) in
-	 CAst.make @@ CCases (RegularStyle, None, item,
+	 CAst.make @@ CCases (Constr.RegularStyle, None, item,
 			      [brlt; breq; brgt])
       | _, _, _ -> failwith "Lists should have the same size"
   in
@@ -769,7 +775,7 @@ let rmake_cmp_def ind mask mind body =
   let items = [mkIdentC x, None, None;
 	       mkIdentC y, None, None] in
   let branches = rbranches_constr id_cmp names decls mask in
-  let body =  CAst.make @@ CCases (RegularStyle, None, items, branches) in
+  let body =  CAst.make @@ CCases (Constr.RegularStyle, None, items, branches) in
     ((dl id_cmp, None), (None, Constrexpr.CStructRec),
      [CLocalAssum([dl (Names.Name x); dl (Names.Name y)],
 		    Default Decl_kinds.Explicit, mkIdentC id_t)],
@@ -790,7 +796,7 @@ let make_mask body =
 
 let generate_rec_ot gref =
   let gindref = Nametab.global gref in
-  let indconstr = Universes.constr_of_global gindref in
+  let indconstr = UnivGen.constr_of_global gindref in
   let indeconstr = EConstr.of_constr indconstr in
   (* retrieve the inductive type *)
   let env = Global.env () in
@@ -813,11 +819,11 @@ let generate_rec_ot gref =
   (* define the equality predicate *)
   let mutual_eq = rmake_eq_mutual ind mask mind ibody in
   (*     fprintf std_formatter "%a" print_inductive_def mutual_eq; *)
-  ComInductive.do_mutual_inductive mutual_eq false false false ComInductive.NonUniformParameters Declarations.Finite;
+  declare_mutual_inductive mutual_eq;
   (* define the strict ordering predicate *)
   let mutual_lt = rmake_lt_mutual ind mask mind ibody in
   (*     fprintf std_formatter "%a" print_inductive_def mutual_lt; *)
-  ComInductive.do_mutual_inductive mutual_lt false false false ComInductive.NonUniformParameters Declarations.Finite;
+  declare_mutual_inductive mutual_lt;
   (* declare the comparison function *)
   let fexpr = rmake_cmp_def ind mask mind ibody in
   ComFixpoint.do_fixpoint Decl_kinds.Global false [(fexpr, [])];
@@ -831,7 +837,7 @@ let generate_rec_ot gref =
 open Declarations
 
 let c_of_id id =
-  Universes.constr_of_global
+  UnivGen.constr_of_global
     (Nametab.global (Libnames.qualid_of_ident id))
 
 exception FoundEqual of int
@@ -902,16 +908,12 @@ let mmake_eq_mutual ind (masks : int list list array) mind =
 	 lconstrs)
 
 let do_proofs goals tac =
-  let env = Global.env () in
-  let evd = Evd.from_env env in
-  let do_proof (name,goal) =
-    let evd, egoal = Constrintern.interp_constr_evars env evd (CAst.make goal) in
-    Lemmas.start_proof name property_kind evd egoal dummy_hook;
-    ignore(Pfedit.by tac);
-    Lemmas.save_proof (Vernacexpr.Proved(Vernacexpr.Transparent,None)) in
-  ignore(List.map do_proof goals)
-
-
+  (* The goals must be proved mutually inductively *)
+  let thms = List.map (fun (name, goal) ->
+      (CAst.make name, None), ([], CAst.make goal)) goals in
+  Lemmas.start_proof_com property_kind thms dummy_hook;
+  List.iter (fun _ -> ignore (Pfedit.by tac)) goals;
+  save_transparent_proof ()
 
 let mprove_refl k ids ids_eq mind =
   let x = Nameops.make_ident "x" None in
@@ -1111,7 +1113,7 @@ let seq_eapply lids : raw_tactic_expr =
     TacAtom (Loc.tag @@
 	     TacApply (true, false,
 		       [(None, (mkIdentC id,
-			 Misctypes.ImplicitBindings [mkIdentC b]))],
+			 Tactypes.ImplicitBindings [mkIdentC b]))],
 		       None))
   in
     TacFun ([Names.Name b], TacFirst (List.map apply lids))
@@ -1123,12 +1125,12 @@ let seq_eapply_sym lids lsyms : raw_tactic_expr =
       TacAtom (Loc.tag @@
 	       TacApply (true, false,
 			 [(None, (mkIdentC id,
-			   Misctypes.ImplicitBindings [mkIdentC b]))],
+			   Tactypes.ImplicitBindings [mkIdentC b]))],
 			 None)),
       [
 	TacAtom (Loc.tag @@
 		 TacApply (true, false,
-			   [(None, (mkIdentC idsym, Misctypes.NoBindings))],
+			   [(None, (mkIdentC idsym, Tactypes.NoBindings))],
 			   None));
 	TacId []
       ])
@@ -1337,7 +1339,7 @@ let mlexi_eqn_constr r ids_cmp carity cmask : branch_expr =
 	  let brlt = dl ([[patc ref_Lt []]], mkIdentC id_Lt) in
 	  let breq = dl ([[patc ref_Eq []]], branch xs ys masks) in
 	  let brgt = dl ([[patc ref_Gt []]], mkIdentC id_Gt) in
-	    CAst.make @@ CCases (RegularStyle, None, item,
+	    CAst.make @@ CCases (Constr.RegularStyle, None, item,
 				 [brlt; breq; brgt])
       | _, _, _ -> failwith "Lists should have the same size"
   in
@@ -1372,7 +1374,7 @@ let mmake_cmp_def k ind masks mind =
     let items = [mkIdentC x, None, None;
 		 mkIdentC y, None, None] in
     let branches = mbranches_constr ids_cmp names decls masks.(i) in
-    CAst.make @@ CCases (RegularStyle, None, items, branches)
+    CAst.make @@ CCases (Constr.RegularStyle, None, items, branches)
   in
   let make_block i body =
     ((dl ids_cmp.(i), None), (None, Constrexpr.CStructRec),
@@ -1416,7 +1418,7 @@ let using_sym ?loc =
        let tac args _ =
 	 let map v =
 	   let id = Tacinterp.Value.cast (topwit Stdarg.wit_ident) v in
-	   (fun ist sigma -> (sigma, (EConstr.of_constr (Universes.constr_of_global (Constrintern.global_reference id)))))
+	   (fun ist sigma -> (sigma, (EConstr.of_constr (UnivGen.constr_of_global (Constrintern.global_reference id)))))
 	 in
 	 let args = List.map map args in
 	 Auto.h_auto None args (Some [])
@@ -1499,7 +1501,7 @@ let generate_mutual_ot gref =
   Coqlib.check_required_library ["Coq";"Classes";"Equivalence"];
   Coqlib.check_required_library ["Containers";"Tactics"];
   let gindref = Nametab.global gref in
-  let indconstr = Universes.constr_of_global gindref in
+  let indconstr = UnivGen.constr_of_global gindref in
   (* retrieve the inductive type *)
   let env = Global.env () in
   let evd = Evd.from_env env in
@@ -1526,12 +1528,12 @@ let generate_mutual_ot gref =
   if_verbose Feedback.msg_notice (str "Inductive kind : " ++ pr_kind kind);
   (* define the equality predicate *)
   let mutual_eq = mmake_eq_mutual ind masks mind in
-  ComInductive.do_mutual_inductive mutual_eq false false false ComInductive.NonUniformParameters Declarations.Finite;
+  declare_mutual_inductive mutual_eq;
   (* prove the Equivalence instance *)
   mprove_Equivalence kind mind;
   (* define the strict ordering predicate *)
   let mutual_lt = mmake_lt_mutual ind masks mind in
-  ComInductive.do_mutual_inductive mutual_lt false false false ComInductive.NonUniformParameters Declarations.Finite;
+  declare_mutual_inductive mutual_lt;
   (* prove the StrictOrder instance *)
   mprove_StrictOrder kind mind;
   (* define the comparison function *)
diff --git a/tests/TestGenerate.v b/tests/TestGenerate.v
new file mode 100644
index 0000000..9eef803
--- /dev/null
+++ b/tests/TestGenerate.v
@@ -0,0 +1,211 @@
+Require Import OrderedTypeEx Generate.
+
+From Coq Require Import Ascii String.
+
+Generate OrderedType ascii.
+Generate OrderedType string.
+
+Open Scope string.
+
+Eval vm_compute in "cat" =?= "dog".
+
+Require Import Sets.
+
+Eval vm_compute in
+    cardinal {"dog"; {"cat"; {"dog"; {"hamster"; {}}}}}.
+
+Inductive tree :=
+| Tree (n : nat) (ts : trees)
+with trees :=
+| TNil
+| TCons (t : tree) (ts : trees).
+
+Generate OrderedType tree.
+
+(** Following is a manual instantiation of OrderedType
+    for [tree] and [trees]. It is useful to manually debug
+    the generic tactics used by Generate OrderedType when
+    something goes wrong. 
+ *)
+(* Inductive tree_eq : tree -> tree -> Prop := *)
+(* | tree_eq_Tree : *)
+(*     forall n n' ts ts', *)
+(*       n === n' -> trees_eq ts ts' -> *)
+(*       tree_eq (Tree n ts) (Tree n' ts') *)
+(* with trees_eq : trees -> trees -> Prop := *)
+(* | trees_eq_TNil : *)
+(*     trees_eq TNil TNil *)
+(* | trees_eq_TCons : *)
+(*     forall t t' ts ts', *)
+(*       tree_eq t t' -> *)
+(*       trees_eq ts ts' -> *)
+(*       trees_eq (TCons t ts) (TCons t' ts'). *)
+
+(* Lemma tree_eq_refl : forall t, tree_eq t t *)
+(* with trees_eq_refl : forall ts, trees_eq ts ts. *)
+(* Proof. *)
+(*   - destruct t; constructor; try reflexivity; auto. *)
+(*   - destruct ts; constructor; try reflexivity; auto. *)
+(* Qed. *)
+(* Lemma tree_eq_sym : forall t t', tree_eq t t' -> tree_eq t' t *)
+(* with trees_eq_sym : forall ts ts', trees_eq ts ts' -> trees_eq ts' ts. *)
+(* Proof. *)
+(*   - intros ? ? H; inversion_clear H; constructor; try symmetry; auto. *)
+(*   - intros ? ? H; inversion_clear H; constructor; try symmetry; auto. *)
+(* Qed. *)
+(* Lemma tree_eq_trans : forall t t' t'', tree_eq t t' -> tree_eq t' t'' -> tree_eq t t'' *)
+(* with trees_eq_trans : forall ts ts' ts'', trees_eq ts ts' -> trees_eq ts' ts'' -> trees_eq ts ts''. *)
+(* Proof. *)
+(*   - intros ? ? ? H H'. *)
+(*     inversion H; subst; clear H. inversion H'; subst; clear H'. *)
+(*     constructor; eauto. transitivity n'; assumption. *)
+(*   - intros ? ? ? H H'; *)
+(*       inversion H; subst; clear H; inversion H'; subst; clear H'. *)
+(*     constructor. *)
+(*     constructor; eauto. *)
+(* Qed. *)
+
+(* Instance tree_eq_Equivalence : Equivalence tree_eq := *)
+(*   Build_Equivalence _ tree_eq_refl tree_eq_sym tree_eq_trans. *)
+(* Instance trees_eq_Equivalence : Equivalence trees_eq := *)
+(*   Build_Equivalence _ trees_eq_refl trees_eq_sym trees_eq_trans. *)
+
+(* Inductive tree_lt : tree -> tree -> Prop := *)
+(* | tree_lt_Tree_1 : *)
+(*     forall n n' ts ts', *)
+(*       n <<< n' -> *)
+(*       tree_lt (Tree n ts) (Tree n' ts') *)
+(* | tree_lt_Tree_2 : *)
+(*     forall n n' ts ts', *)
+(*       n === n' -> trees_lt ts ts' -> *)
+(*       tree_lt (Tree n ts) (Tree n' ts') *)
+(* with trees_lt : trees -> trees -> Prop := *)
+(* | trees_lt_TNil_TCons : *)
+(*     forall t ts, *)
+(*       trees_lt TNil (TCons t ts) *)
+(* | trees_lt_TCons_1 : *)
+(*     forall t t' ts ts', *)
+(*       tree_lt t t' -> *)
+(*       trees_lt (TCons t ts) (TCons t' ts') *)
+(* | trees_lt_TCons_2 : *)
+(*     forall t t' ts ts', *)
+(*       t === t' -> *)
+(*       trees_lt ts ts' -> *)
+(*       trees_lt (TCons t ts) (TCons t' ts'). *)
+
+(* Lemma tree_lt_irrefl : forall t t', tree_lt t t' -> t === t' -> False *)
+(* with trees_lt_irrefl : forall ts ts', trees_lt ts ts' -> ts === ts' -> False. *)
+(* Proof. *)
+(*   - intros ? ? Hlt Heq; inversion Heq; subst; clear Heq; *)
+(*       inversion Hlt; subst; clear Hlt; eauto; order. *)
+(*   - intros ? ? Hlt Heq; inversion Heq; subst; clear Heq; *)
+(*       inversion Hlt; subst; clear Hlt; eauto. *)
+(* Qed. *)
+
+(* Lemma tree_eq_lt : forall t t' t'', t === t' -> tree_lt t t'' -> tree_lt t' t'' *)
+(* with trees_eq_lt : forall ts ts' ts'', ts === ts' -> trees_lt ts ts'' -> trees_lt ts' ts''. *)
+(* Proof. *)
+(*   - intros ? ? ? Heq Hlt; inversion Heq; subst; clear Heq; *)
+(*       inversion Hlt; subst; clear Hlt. *)
+(*     constructor; order. *)
+(*     constructor 2; eauto; order. *)
+(*   - intros ? ? ? Heq Hlt; inversion Heq; subst; clear Heq; *)
+(*       inversion Hlt; subst; clear Hlt. *)
+(*     constructor. *)
+(*     constructor; eauto; order. *)
+(*     constructor 3; eauto; order. *)
+(* Qed. *)
+(* Lemma tree_eq_gt : forall t t' t'', t === t' -> tree_lt t'' t -> tree_lt t'' t' *)
+(* with trees_eq_gt : forall ts ts' ts'', ts === ts' -> trees_lt ts'' ts -> trees_lt ts'' ts'. *)
+(* Proof. *)
+(*   - intros ? ? ? Heq Hlt; inversion Heq; subst; clear Heq; *)
+(*       inversion Hlt; subst; clear Hlt. *)
+(*     constructor. now rewrite <- H. *)
+(*     constructor 2; eauto; order. *)
+(*   - intros ? ? ? Heq Hlt; inversion Heq; subst; clear Heq; *)
+(*       inversion Hlt; subst; clear Hlt. *)
+(*     constructor. *)
+(*     constructor; eauto; order. *)
+(*     constructor 3; eauto; order. *)
+(* Qed. *)
+
+(* Lemma tree_lt_trans : forall t t' t'', tree_lt t t' -> tree_lt t' t'' -> tree_lt t t'' *)
+(* with trees_lt_trans : forall ts ts' ts'', trees_lt ts ts' -> trees_lt ts' ts'' -> trees_lt ts ts''. *)
+(* Proof. *)
+(*   - intros ? ? ? H1 H2; inversion H1; subst; clear H1; *)
+(*       inversion H2; subst; clear H2. *)
+(*     constructor; etransitivity; eauto. *)
+(*     constructor; now rewrite <- H3. *)
+(*     constructor; now rewrite H. *)
+(*     constructor 2. now transitivity n'. eauto. *)
+(*   - intros ? ? ? H1 H2; inversion H1; subst; clear H1; *)
+(*       inversion H2; subst; clear H2; eauto. *)
+(*     constructor. constructor. *)
+(*     constructor; eauto. *)
+(*     constructor; eauto using tree_eq_gt. *)
+(*     constructor; symmetry in H; eauto using tree_eq_lt. *)
+(*     constructor 3; eauto. order. *)
+(* Qed. *)
+
+(* Instance tree_lt_StrictOrder : StrictOrder tree_lt tree_eq := *)
+(*   Build_StrictOrder _ _ _ _ tree_lt_trans tree_lt_irrefl. *)
+(* Instance trees_lt_StrictOrder : StrictOrder trees_lt trees_eq := *)
+(*   Build_StrictOrder _ _ _ _ trees_lt_trans trees_lt_irrefl. *)
+
+(* Fixpoint tree_cmp (t t' : tree) : comparison := *)
+(*   match t with *)
+(*   | Tree n ts => *)
+(*     match t' with *)
+(*     | Tree n' ts' => *)
+(*       match n =?= n' with *)
+(*       | Eq => trees_cmp ts ts' *)
+(*       | c => c *)
+(*       end *)
+(*     end *)
+(*   end *)
+(* with trees_cmp (ts ts' : trees) : comparison := *)
+(*   match ts with *)
+(*   | TNil => *)
+(*     match ts' with *)
+(*     | TNil => Eq *)
+(*     | TCons _ _ => Lt *)
+(*     end *)
+(*   | TCons t ts => *)
+(*     match ts' with *)
+(*     | TNil => Gt *)
+(*     | TCons t' ts' => *)
+(*       match tree_cmp t t' with *)
+(*       | Eq => trees_cmp ts ts' *)
+(*       | c => c *)
+(*       end *)
+(*     end *)
+(*   end. *)
+
+(* Lemma tree_compare_spec : forall t t', compare_spec tree_eq tree_lt t t' (tree_cmp t t') *)
+(* with trees_compare_spec : forall ts ts', compare_spec trees_eq trees_lt ts ts' (trees_cmp ts ts'). *)
+(* Proof. *)
+(*   - destruct t; destruct t'; simpl. *)
+(*     destruct (compare_dec n n0). *)
+(*     constructor; constructor; auto. *)
+(*     destruct (trees_compare_spec ts ts0); constructor. *)
+(*     constructor 2; auto. *)
+(*     constructor; auto. *)
+(*     constructor 2; auto. *)
+(*     constructor; constructor; auto. *)
+(*   - destruct ts; destruct ts'; simpl. *)
+(*     constructor; constructor. *)
+(*     constructor; constructor. *)
+(*     constructor; constructor. *)
+(*     destruct (tree_compare_spec t t0). *)
+(*     constructor; constructor; auto. *)
+(*     destruct (trees_compare_spec ts ts'); constructor. *)
+(*     constructor 3; auto. *)
+(*     constructor; auto. *)
+(*     constructor 3; auto. *)
+(*     constructor; constructor; auto. *)
+(* Qed. *)
+
+(* Instance tree_OrderedType : OrderedType tree := *)
+(*   Build_OrderedType _ tree_eq tree_lt _ _ tree_cmp tree_compare_spec. *)
+(* Instance trees_OrderedType : OrderedType trees := *)
+(*   Build_OrderedType _ trees_eq trees_lt _ _ trees_cmp trees_compare_spec. *)
\ No newline at end of file
diff --git a/theories/OrderedTypeEx.v b/theories/OrderedTypeEx.v
index 695c92f..9037758 100644
--- a/theories/OrderedTypeEx.v
+++ b/theories/OrderedTypeEx.v
@@ -279,7 +279,7 @@ Program Instance prod_UsualStrictOrder
   `(UsualOrderedType A, UsualOrderedType B) :
   StrictOrder (@prod_lt A B (@Logic.eq _) _lt _lt) (@Logic.eq _).
 Next Obligation. (* transitivity *)
-  do 4 intro; inversion_clear 0; intro; inversion_clear 0;
+  do 4 intro; inversion_clear H1; intro H1; inversion_clear H1;
     subst; try (tconstructor (auto; solve_by_trans_modulo)).
 Qed.
 Next Obligation. (* irreflexivity *)
@@ -493,7 +493,7 @@ Program Instance list_StrictOrder `(OrderedType A) :
   StrictOrder (@list_lt A _lt _eq) (@list_eq A _).
 Next Obligation. (* transitivity *)
   intros nx ny nz nHlt1; revert nz; induction nHlt1;
-    do 2 intro; inversion_clear 0;
+    intros nz nHlt2; inversion_clear nHlt2;
       try tconstructor (idtac; solve_by_trans_modulo).
   constructor 3; order.
 Qed.
diff --git a/theories/Tactics.v b/theories/Tactics.v
index 7b6f0ca..a170852 100644
--- a/theories/Tactics.v
+++ b/theories/Tactics.v
@@ -62,16 +62,24 @@ Tactic Notation "tconstructor" tactic(t) :=
 (** * Tactics for inductives without recursion, nor parameters *)
 
 (** ** Equivalence *)
-Ltac inductive_refl := try unfold Reflexive;
-  destruct 0; try tconstructor (reflexivity).
+Ltac inductive_refl :=
+  try unfold Reflexive;
+  let nx := fresh "x" in
+  intro nx; destruct nx; try tconstructor (reflexivity).
 
-Ltac inductive_sym := try unfold Symmetric;
-  do 3 intro; destruct 0;
+Ltac inductive_sym :=
+  try unfold Symmetric;
+  let nH := fresh "H" in
+  intros ? ? nH; destruct nH;
     try tconstructor (symmetry; assumption).
 
-Ltac inductive_trans := try unfold Transitive;
-  do 4 intro; inversion_clear 0; intro; inversion_clear 0;
-    try tconstructor (eapply transitivity; eassumption).
+Ltac inductive_trans :=
+  try unfold Transitive;
+  let nH1 := fresh "H1" in
+  intros ? ? ? nH1; inversion_clear nH1;
+  let nH2 := fresh "H2" in
+  intro nH2; inversion_clear nH2;
+  try tconstructor (eapply transitivity; eassumption).
 
 (** ** StrictOrder *)
 Ltac solve_by_trans_modulo :=
@@ -79,13 +87,16 @@ Ltac solve_by_trans_modulo :=
     | H1 : ?R ?A ?B, H2 : ?R ?B ?C |- ?R ?A ?C =>
       transitivity B; eassumption
     | H1 : ?R ?A ?B, H2 : ?R' ?B ?C |- ?R ?A ?C =>
-      apply eq_gt with B; assumption
+      exact (@eq_gt _ _ B C A H2 H1)
     | H1 : ?R ?A ?B, H2 : ?R' ?B ?C |- ?R' ?A ?C =>
-      apply eq_lt with B; [symmetry|]; assumption
+      exact (@eq_lt _ _ B A C (Equivalence_Symmetric _ _ H1) H2)
  end.
 Ltac inductive_lexico_trans :=
-  do 4 intro; inversion_clear 0; intro; inversion_clear 0;
-    try tconstructor (idtac; solve_by_trans_modulo).
+  let nH1 := fresh "H1" in
+  intros ? ? ? nH1; inversion_clear nH1;
+  let nH2 := fresh "H2" in
+  intros nH2; inversion_clear nH2;
+  try tconstructor (idtac; solve_by_trans_modulo).
 
 Ltac solve_by_irrefl :=
   match goal with
@@ -95,8 +106,10 @@ Ltac solve_by_irrefl :=
       apply (gt_not_eq (x:=A) (y:=A0)); assumption
   end.
 Ltac inductive_irrefl :=
-  do 3 intro; inversion_clear 0; intro; inversion_clear 0;
-    try solve_by_irrefl.
+  let nHlt := fresh "Hlt" in
+  let nHeq := fresh "Heq" in
+  intros ? ? nHlt; inversion_clear nHlt; intro nHeq; inversion_clear nHeq;
+  try solve_by_irrefl.
 
 (** ** compare_spec *)
 Ltac solve_compare_spec_match :=
@@ -115,17 +128,21 @@ Ltac solve_compare_spec :=
 (** * Tactics for inductives with recursion, but no parameters *)
 
 (** ** Equivalence *)
-Ltac rinductive_refl := try unfold Reflexive;
-  induction 0; try tconstructor (try assumption; reflexivity).
+Ltac rinductive_refl :=
+  try unfold Reflexive;
+  let nx := fresh "x" in
+  intro nx; induction nx; try tconstructor (try assumption; reflexivity).
 
-Ltac rinductive_sym := try unfold Symmetric;
-  do 3 intro; induction 0; try tconstructor (try symmetry; assumption).
+Ltac rinductive_sym :=
+  try unfold Symmetric;
+  let nH := fresh "H" in
+  intros ? ? nH; induction nH; try tconstructor (try symmetry; assumption).
 
 Ltac rinductive_trans :=
   let nx := fresh "x" in let ny := fresh "y" in let nz := fresh "z" in
-    let nHeq1 := fresh "Heq1" in
+    let nHeq1 := fresh "Heq1" in let nHeq2 := fresh "Heq2" in
       intros nx ny nz nHeq1; revert nz; induction nHeq1;
-        do 2 intro; inversion_clear 0;
+        intros ? nHeq2; inversion_clear nHeq2;
           try (tconstructor (solve [auto | eapply transitivity; eassumption])).
 
 (** ** StrictOrder *)
@@ -137,9 +154,9 @@ Ltac solve_eq_lt  t_eq_sym t_eq_trans :=
   ].
 Ltac rinductive_eq_lt t_eq_sym t_eq_trans :=
   let nx := fresh "x" in let nx' := fresh "x'" in let ny := fresh "y" in
-    let nHlt := fresh "Heq" in
+    let nHeq := fresh "Heq" in let nHlt := fresh "Hlt" in
       intros nx nx' ny nHeq; revert ny; induction nHeq;
-        do 2 intro; inversion_clear 0;
+        intros ? nHlt; inversion_clear nHlt;
           try tconstructor (solve_eq_lt t_eq_sym t_eq_trans).
 
 Ltac solve_eq_gt t_eq_trans :=
@@ -151,34 +168,52 @@ Ltac solve_eq_gt t_eq_trans :=
   ].
 Ltac rinductive_eq_gt t_eq_trans :=
   let nx := fresh "x" in let nx' := fresh "x'" in let ny := fresh "y" in
-    let nHeq := fresh "Heq" in
+    let nHeq := fresh "Heq" in let nHlt := fresh "Hlt" in
       intros nx nx' ny nHeq; revert ny; induction nHeq;
-        do 2 intro; inversion_clear 0;
+        intros ? nHlt; inversion_clear nHlt;
           try tconstructor (solve_eq_gt t_eq_trans).
 
+(** Legacy tactic: stopped working because of change in apply/unification ? *)
+(* Ltac rsolve_by_trans_modulo *)
+(*   t_eq_sym t_eq_trans t_eq_gt t_eq_lt := *)
+(*   match goal with *)
+(*     | H1 : ?R ?A ?B, H2 : ?R ?B ?C |- ?R ?A ?C => *)
+(*       first [apply t_eq_trans with B | transitivity B]; eassumption *)
+(*     | H1 : ?R ?A ?B, H2 : ?R' ?B ?C |- ?R ?A ?C => *)
+(*       first [apply t_eq_gt with B | apply eq_gt with B]; assumption *)
+(*     | H1 : ?R ?A ?B, H2 : ?R' ?B ?C |- ?R' ?A ?C => *)
+(*       first [apply t_eq_lt with B; [apply t_eq_sym |] | *)
+(*         apply eq_lt with B; [symmetry |]]; assumption *)
+(*     | IH : forall z, ?R _ _ -> ?R _ _ |- ?R _ _ => *)
+(*       apply IH; assumption *)
+(*  end. *)
 Ltac rsolve_by_trans_modulo
   t_eq_sym t_eq_trans t_eq_gt t_eq_lt :=
   match goal with
-    | H1 : ?R ?A ?B, H2 : ?R ?B ?C |- ?R ?A ?C =>
-      first [apply t_eq_trans with B | transitivity B]; eassumption
-    | H1 : ?R ?A ?B, H2 : ?R' ?B ?C |- ?R ?A ?C =>
-      first [apply t_eq_gt with B | apply eq_gt with B]; assumption
-    | H1 : ?R ?A ?B, H2 : ?R' ?B ?C |- ?R' ?A ?C =>
-      first [apply t_eq_lt with B; [apply t_eq_sym |] |
-        apply eq_lt with B; [symmetry |]]; assumption
-    | IH : forall z, ?R _ _ -> ?R _ _ |- ?R _ _ =>
-      apply IH; assumption
- end.
+  | H1 : ?R ?A ?B, H2 : ?R ?B ?C |- ?R ?A ?C =>
+    (apply t_eq_trans with B; assumption) ||
+    (transitivity B; eassumption)
+  | H1 : ?R ?A ?B, H2 : ?R' ?B ?C |- ?R ?A ?C =>
+    (apply t_eq_gt with B; assumption) ||
+      exact (@eq_gt _ _ B C A H2 H1)
+  | H1 : ?R ?A ?B, H2 : ?R' ?B ?C |- ?R' ?A ?C =>
+    (apply t_eq_lt with B; [ apply t_eq_sym | ]; assumption) ||
+    exact (@eq_lt _ _ B A C (Equivalence_Symmetric _ _ H1) H2)
+  | IH : forall z, ?R _ _ -> ?R _ _ |- ?R _ _ =>
+    apply IH; assumption
+  end.
+
 Ltac rinductive_lexico_trans t_eq_sym t_eq_trans t_eq_gt t_eq_lt :=
   let nx := fresh "x" in let ny := fresh "y" in let nz := fresh "z" in
-    let nHlt1 := fresh "Hlt1" in
+    let nHlt1 := fresh "Hlt1" in let nHlt2 := fresh "Hlt2" in
       intros nx ny nz nHlt1; revert nz; induction nHlt1;
-        do 2 intro; inversion_clear 0;
+        intros ? nHlt2; inversion_clear nHlt2;
           try tconstructor (idtac; rsolve_by_trans_modulo
             t_eq_sym t_eq_trans t_eq_gt t_eq_lt).
 
 Ltac rinductive_irrefl :=
-  do 3 intro; induction 0; intro; inversion_clear 0;
+  let nHlt := fresh "Hlt" in let nHeq := fresh "Heq" in
+  intros ? ? nHlt; induction nHlt; intro nHeq; inversion_clear nHeq;
     auto; solve_by_irrefl.
 
 (** ** compare_spec *)
@@ -203,39 +238,50 @@ Ltac rsolve_compare_spec t_eq_sym :=
 
 (** ** Equivalence *)
 Ltac minductive_refl :=
-  induction 0; constructor; auto; reflexivity.
+  let nx := fresh "x" in
+  intro nx; induction nx; constructor; auto; reflexivity.
 Ltac minductive_sym :=
-  do 3 intro; induction 0; tconstructor (try symmetry); auto.
+  let nH := fresh "H" in
+  intros ? ? nH; induction nH; tconstructor (try symmetry); auto.
 Ltac minductive_trans :=
   let nx := fresh "x" in let ny := fresh "y" in
-    let nz := fresh "z" in let nHeq1 := fresh "Heq1" in
+    let nz := fresh "z" in let nHeq1 := fresh "Heq1" in let nHeq2 := fresh "Heq2" in
       intros nx ny nz nHeq1; revert nz;
         induction nHeq1;
-          do 2 intro; inversion_clear 0; constructor;
+          intros ? nHeq2; inversion_clear nHeq2; constructor;
             solve [eauto | eapply transitivity; eassumption].
 
 (** ** StrictOrder *)
 Ltac minductive_irrefl :=
-  do 3 intro; induction 0; intro;
-    inversion_clear 0; eauto; solve_by_irrefl.
+  let nHlt := fresh "Hlt" in let nHeq := fresh "Heq" in
+  intros ? ? nHlt; induction nHlt; intro nHeq;
+  inversion_clear nHeq; eauto; solve_by_irrefl.
 Ltac msolve_eq_lt s :=
   solve [
-    eapply transitivity; [symmetry|]; eassumption |
-      eapply eq_lt; eassumption |
-        s
-  ].
+      eapply transitivity; [symmetry|]; eassumption |
+      match goal with
+      | E: ?N === ?M, L: ?N <<< ?P |- ?M <<< ?P =>
+        exact (@eq_lt _ _ _ _ _ E L)
+      end
+      (* eapply eq_lt; eassumption | *) |
+      s
+    ].
 Ltac msolve_eq_gt s :=
   solve [
-    s |
+      s |
       eapply transitivity; eassumption |
-        eapply eq_gt; eassumption |
-          auto
+      match goal with
+      | E: ?N === ?M, L: ?P <<< ?N |- ?P <<< ?M =>
+        exact (@eq_gt _ _ _ _ _ E L)
+      end
+      (* eapply eq_gt; eassumption *) |
+      auto
   ].
 Ltac minductive_eq_lt_gt s :=
   let nx := fresh "x" in let nx' := fresh "x'" in
-    let ny := fresh "y" in let nHlt := fresh "Heq" in
+    let ny := fresh "y" in let nHeq := fresh "Heq" in let nHlt := fresh "Hlt" in
       intros nx nx' ny nHeq; revert ny; induction nHeq;
-        do 2 intro; inversion_clear 0;
+        intros ? nHlt; inversion_clear nHlt;
           tconstructor s.
 Ltac msolve_by_trans_modulo strans seqgt seqlt :=
   match goal with
@@ -244,21 +290,22 @@ Ltac msolve_by_trans_modulo strans seqgt seqlt :=
         (first [ strans B | transitivity B ]); eassumption
   | H1:?R ?A ?B, H2:?R' ?B ?C
     |- ?R ?A ?C =>
-        (first [ seqgt B | apply eq_gt with B ]); assumption
+        (first [ seqgt B | exact (@eq_gt _ _ _ _ _ H2 H1) ]); assumption
   | H1:?R ?A ?B, H2:?R' ?B ?C
     |- ?R' ?A ?C =>
         (first
-          [ seqlt B | apply eq_lt with B; [ symmetry  in |- * | idtac ] ]);
+           [ seqlt B |
+             exact (@eq_lt _ _ _ _ _ (Equivalence_Symmetric _ _ H1) H2) ]);
         assumption
-    | IH:forall x y z, ?R _ _ -> ?R _ _ -> ?R _ _ |- ?R _ _ =>
-      eapply IH; eassumption
+  | IH:forall x y z, ?R _ _ -> ?R _ _ -> ?R _ _ |- ?R _ _ =>
+    eapply IH; eassumption
   end.
 Ltac minductive_lexico_trans sstrans seqgt seqlt :=
   let nx := fresh "x" in let ny := fresh "y" in
-    let nz := fresh "z" in let nHlt1 := fresh "Hlt1" in
+    let nz := fresh "z" in let nHlt1 := fresh "Hlt1" in let nHlt2 := fresh "Hlt2" in
       intros nx ny nz nHlt1; revert nz; induction nHlt1;
-        do 2 intro; inversion_clear 0;
-          tconstructor (msolve_by_trans_modulo sstrans seqgt seqlt).
+      intros ? nHlt2; inversion_clear nHlt2;
+      once (constructor; msolve_by_trans_modulo sstrans seqgt seqlt).
 
 (** ** compare_spec *)
 Ltac msolve_compare_spec_match s :=