Use properly fresh names for Scheme Equality

4 files changed, 220 insertions, 219 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cb2e607012..70cea89ccb 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1044,12 +1044,15 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
           end
   end
 
-let intro_gen n m f d = intro_then_gen n m f d (fun _ -> Proofview.tclUNIT ())
+let drop_intro_name (_ : Id.t) = Proofview.tclUNIT ()
+
+let intro_gen n m f d = intro_then_gen n m f d drop_intro_name
 let intro_mustbe_force id = intro_gen (NamingMustBe (CAst.make id)) MoveLast true false
-let intro_using id = intro_gen (NamingBasedOn (id, Id.Set.empty)) MoveLast false false
+let intro_using_then id = intro_then_gen (NamingBasedOn (id, Id.Set.empty)) MoveLast false false
+let intro_using id = intro_using_then id drop_intro_name
 
 let intro_then = intro_then_gen (NamingAvoid Id.Set.empty) MoveLast false false
-let intro = intro_gen (NamingAvoid Id.Set.empty) MoveLast false false
+let intro = intro_then drop_intro_name
 let introf = intro_gen (NamingAvoid Id.Set.empty) MoveLast true false
 let intro_avoiding l = intro_gen (NamingAvoid l) MoveLast false false
 
@@ -1065,6 +1068,11 @@ let rec intros_using = function
   | []     -> Proofview.tclUNIT()
   | str::l -> Tacticals.New.tclTHEN (intro_using str) (intros_using l)
 
+let rec intros_using_then_helper tac acc = function
+  | []     -> tac (List.rev acc)
+  | str::l -> intro_using_then str (fun str' -> intros_using_then_helper tac (str'::acc) l)
+let intros_using_then l tac = intros_using_then_helper tac [] l
+
 let intros = Tacticals.New.tclREPEAT intro
 
 let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac =
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 5b397b15d0..00739306a7 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -65,9 +65,11 @@ val intro_avoiding       : Id.Set.t -> unit Proofview.tactic
 
 val intro_replacing      : Id.t -> unit Proofview.tactic
 val intro_using          : Id.t -> unit Proofview.tactic
+val intro_using_then     : Id.t -> (Id.t -> unit Proofview.tactic) -> unit Proofview.tactic
 val intro_mustbe_force   : Id.t -> unit Proofview.tactic
 val intro_then           : (Id.t -> unit Proofview.tactic) -> unit Proofview.tactic
 val intros_using         : Id.t list -> unit Proofview.tactic
+val intros_using_then    : Id.t list -> (Id.t list -> unit Proofview.tactic) -> unit Proofview.tactic
 val intros_replacing     : Id.t list -> unit Proofview.tactic
 val intros_possibly_replacing : Id.t list -> unit Proofview.tactic
 
diff --git a/test-suite/bugs/closed/bug_12763.v b/test-suite/bugs/closed/bug_12763.v
new file mode 100644
index 0000000000..6cbcc0d3b0
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12763.v
@@ -0,0 +1,6 @@
+Inductive bool_list := S (y : bool) (l : bool_list) | O.
+Scheme Equality for bool_list.
+
+Set Mangle Names.
+Scheme Equality for nat.
+Scheme Equality for list.
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index f47cdd8bf0..7a7e7d6e35 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -556,11 +556,17 @@ let list_id l = List.fold_left ( fun a decl -> let s' =
               Id.of_string (s'^"_lb"))
             ::a
     ) [] l
+
+let avoid_of_list_id list_id =
+  List.fold_left (fun avoid (s,seq,sbl,slb) ->
+      List.fold_left (fun avoid id -> Id.Set.add id avoid)
+        avoid [s;seq;sbl;slb])
+    Id.Set.empty list_id
+
 (*
   build the right eq_I A B.. N eq_A .. eq_N
 *)
-let eqI ind l =
-  let list_id = list_id l in
+let eqI ind list_id =
   let eA = Array.of_list((List.map (fun (s,_,_,_) -> mkVar s) list_id)@
                            (List.map (fun (_,seq,_,_)-> mkVar seq) list_id ))
   and e = match lookup_scheme beq_scheme_kind ind with
@@ -568,7 +574,7 @@ let eqI ind l =
   | None ->
     user_err ~hdr:"AutoIndDecl.eqI"
       (str "The boolean equality on " ++ Printer.pr_inductive (Global.env ()) ind ++ str " is needed.");
-  in (if Array.equal Constr.equal eA [||] then e else mkApp(e,eA))
+  in mkApp(e,eA)
 
 (**********************************************************************)
 (* Boolean->Leibniz *)
@@ -576,12 +582,12 @@ let eqI ind l =
 open Namegen
 
 let compute_bl_goal ind lnamesparrec nparrec =
-  let eqI = eqI ind lnamesparrec in
   let list_id = list_id lnamesparrec in
-  let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in
+  let eqI = eqI ind list_id in
+  let avoid = avoid_of_list_id list_id in
+  let x = next_ident_away (Id.of_string "x") avoid in
+  let y = next_ident_away (Id.of_string "y") (Id.Set.add x avoid) in
   let create_input c =
-    let x = next_ident_away (Id.of_string "x") avoid and
-        y = next_ident_away (Id.of_string "y") avoid in
       let bl_typ = List.map (fun (s,seq,_,_) ->
         mkNamedProd (make_annot x Sorts.Relevant) (mkVar s) (
             mkNamedProd (make_annot y Sorts.Relevant) (mkVar s) (
@@ -607,88 +613,74 @@ let compute_bl_goal ind lnamesparrec nparrec =
         in
         mkNamedProd x (RelDecl.get_type decl) a) eq_input lnamesparrec
     in
-      let n = next_ident_away (Id.of_string "x") avoid and
-          m = next_ident_away (Id.of_string "y") avoid in
       let u = Univ.Instance.empty in
      create_input (
-        mkNamedProd (make_annot n Sorts.Relevant) (mkFullInd (ind,u) nparrec) (
-          mkNamedProd (make_annot m Sorts.Relevant) (mkFullInd (ind,u) (nparrec+1)) (
+        mkNamedProd (make_annot x Sorts.Relevant) (mkFullInd (ind,u) nparrec) (
+          mkNamedProd (make_annot y Sorts.Relevant) (mkFullInd (ind,u) (nparrec+1)) (
             mkArrow
-              (mkApp(eq (),[|bb ();mkApp(eqI,[|mkVar n;mkVar m|]);tt ()|]))
+              (mkApp(eq (),[|bb ();mkApp(eqI,[|mkVar x;mkVar y|]);tt ()|]))
               Sorts.Relevant
-              (mkApp(eq (),[|mkFullInd (ind,u) (nparrec+3);mkVar n;mkVar m|]))
+              (mkApp(eq (),[|mkFullInd (ind,u) (nparrec+3);mkVar x;mkVar y|]))
         )))
 
 let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec =
   let list_id = list_id lnamesparrec in
-  let avoid = ref [] in
-      let first_intros =
-        ( List.map (fun (s,_,_,_) -> s ) list_id ) @
-        ( List.map (fun (_,seq,_,_ ) -> seq) list_id ) @
-        ( List.map (fun (_,_,sbl,_ ) -> sbl) list_id )
-      in
-      let fresh_id s gl =
-          let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in
-          avoid := fresh::(!avoid); fresh
-      in
-      Proofview.Goal.enter begin fun gl ->
-      let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
-      let freshn = fresh_id (Id.of_string "x") gl in
-      let freshm = fresh_id (Id.of_string "y") gl in
-      let freshz = fresh_id (Id.of_string "Z") gl in
-  (* try with *)
-      Tacticals.New.tclTHENLIST [ intros_using fresh_first_intros;
-                     intro_using freshn ;
-                     induct_on (EConstr.mkVar freshn);
-                     intro_using freshm;
-                     destruct_on (EConstr.mkVar freshm);
-                     intro_using freshz;
-                     intros;
-                     Tacticals.New.tclTRY (
-                      Tacticals.New.tclORELSE reflexivity my_discr_tac
-                     );
-                     simpl_in_hyp (freshz,Locus.InHyp);
-(*
+  let first_intros =
+    ( List.map (fun (s,_,_,_) -> s ) list_id )
+    @ ( List.map (fun (_,seq,_,_ ) -> seq) list_id )
+    @ ( List.map (fun (_,_,sbl,_ ) -> sbl) list_id )
+  in
+  intros_using_then first_intros begin fun fresh_first_intros ->
+    Tacticals.New.tclTHENLIST [
+        intro_using_then (Id.of_string "x") (fun freshn -> induct_on (EConstr.mkVar freshn));
+        intro_using_then (Id.of_string "y") (fun freshm -> destruct_on (EConstr.mkVar freshm));
+        intro_using_then (Id.of_string "Z") begin fun freshz ->
+          Tacticals.New.tclTHENLIST [
+              intros;
+              Tacticals.New.tclTRY (
+                  Tacticals.New.tclORELSE reflexivity my_discr_tac
+                );
+              simpl_in_hyp (freshz,Locus.InHyp);
+              (*
 repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
-*)
-                    Tacticals.New.tclREPEAT (
-                      Tacticals.New.tclTHENLIST [
-                         Simple.apply_in freshz (EConstr.of_constr (andb_prop()));
-                         Proofview.Goal.enter begin fun gl ->
-                           let fresht = fresh_id (Id.of_string "Z") gl in
-                            destruct_on_as (EConstr.mkVar freshz)
-                                  (IntroOrPattern [[CAst.make @@ IntroNaming (IntroIdentifier fresht);
-                                    CAst.make @@ IntroNaming (IntroIdentifier freshz)]])
-                         end
-                        ]);
-(*
+               *)
+              Tacticals.New.tclREPEAT (
+                  Tacticals.New.tclTHENLIST [
+                      Simple.apply_in freshz (EConstr.of_constr (andb_prop()));
+                      destruct_on_as (EConstr.mkVar freshz)
+                        (IntroOrPattern [[CAst.make @@ IntroNaming (IntroFresh (Id.of_string "Z"));
+                                          CAst.make @@ IntroNaming (IntroIdentifier freshz)]])
+                ]);
+              (*
   Ci a1 ... an = Ci b1 ... bn
  replace bi with ai; auto || replace bi with ai by  apply typeofbi_prod ; auto
-*)
-                      Proofview.Goal.enter begin fun gl ->
-                        let concl = Proofview.Goal.concl gl in
-                        let sigma = Tacmach.New.project gl in
-                        match EConstr.kind sigma concl with
-                        | App (c,ca) -> (
-                          match EConstr.kind sigma c with
-                          | Ind (indeq, u) ->
-                              if GlobRef.equal (GlobRef.IndRef indeq) Coqlib.(lib_ref "core.eq.type")
-                              then
-                                Tacticals.New.tclTHEN
-                                  (do_replace_bl bl_scheme_key ind
-                                     (!avoid)
-                                     nparrec (ca.(2))
-                                     (ca.(1)))
-                                  Auto.default_auto
-                              else
-                                Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.")
-                          | _ -> Tacticals.New.tclZEROMSG (str" Failure while solving Boolean->Leibniz.")
-                        )
-                        | _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.")
-                      end
+               *)
+              Proofview.Goal.enter begin fun gl ->
+                let concl = Proofview.Goal.concl gl in
+                let sigma = Tacmach.New.project gl in
+                match EConstr.kind sigma concl with
+                | App (c,ca) -> (
+                  match EConstr.kind sigma c with
+                  | Ind (indeq, u) ->
+                     if GlobRef.equal (GlobRef.IndRef indeq) Coqlib.(lib_ref "core.eq.type")
+                     then
+                       Tacticals.New.tclTHEN
+                         (do_replace_bl bl_scheme_key ind
+                            (List.rev fresh_first_intros)
+                            nparrec (ca.(2))
+                            (ca.(1)))
+                         Auto.default_auto
+                     else
+                       Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.")
+                  | _ -> Tacticals.New.tclZEROMSG (str" Failure while solving Boolean->Leibniz.")
+                )
+                | _ -> Tacticals.New.tclZEROMSG (str "Failure while solving Boolean->Leibniz.")
+                end
 
-                    ]
-      end
+            ]
+          end
+      ]
+    end
 
 let bl_scheme_kind_aux = ref (fun _ -> failwith "Undefined")
 
@@ -729,11 +721,11 @@ let _ = bl_scheme_kind_aux := fun () -> bl_scheme_kind
 let compute_lb_goal ind lnamesparrec nparrec =
   let list_id = list_id lnamesparrec in
   let eq = eq () and tt = tt () and bb = bb () in
-  let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in
-  let eqI = eqI ind lnamesparrec in
+  let avoid = avoid_of_list_id list_id in
+  let eqI = eqI ind list_id in
+  let x = next_ident_away (Id.of_string "x") avoid in
+  let y = next_ident_away (Id.of_string "y") (Id.Set.add x avoid) in
     let create_input c =
-      let x = next_ident_away (Id.of_string "x") avoid and
-          y = next_ident_away (Id.of_string "y") avoid in
       let lb_typ = List.map (fun (s,seq,_,_) ->
         mkNamedProd (make_annot x Sorts.Relevant) (mkVar s) (
             mkNamedProd (make_annot y Sorts.Relevant) (mkVar s) (
@@ -760,73 +752,62 @@ let compute_lb_goal ind lnamesparrec nparrec =
           in
           mkNamedProd x (RelDecl.get_type decl)  a) eq_input lnamesparrec
     in
-      let n = next_ident_away (Id.of_string "x") avoid and
-          m = next_ident_away (Id.of_string "y") avoid in
       let u = Univ.Instance.empty in
       create_input (
-        mkNamedProd (make_annot n Sorts.Relevant) (mkFullInd (ind,u) nparrec) (
-          mkNamedProd (make_annot m Sorts.Relevant) (mkFullInd (ind,u) (nparrec+1)) (
+        mkNamedProd (make_annot x Sorts.Relevant) (mkFullInd (ind,u) nparrec) (
+          mkNamedProd (make_annot y Sorts.Relevant) (mkFullInd (ind,u) (nparrec+1)) (
             mkArrow
-              (mkApp(eq,[|mkFullInd (ind,u) (nparrec+2);mkVar n;mkVar m|]))
+              (mkApp(eq,[|mkFullInd (ind,u) (nparrec+2);mkVar x;mkVar y|]))
               Sorts.Relevant
-              (mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|]))
+              (mkApp(eq,[|bb;mkApp(eqI,[|mkVar x;mkVar y|]);tt|]))
         )))
 
 let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec =
   let list_id = list_id lnamesparrec in
-    let avoid = ref [] in
-      let first_intros =
-        ( List.map (fun (s,_,_,_) -> s ) list_id ) @
-        ( List.map (fun (_,seq,_,_) -> seq) list_id ) @
-        ( List.map (fun (_,_,_,slb) -> slb) list_id )
-      in
-      let fresh_id s gl =
-          let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in
-          avoid := fresh::(!avoid); fresh
-      in
-      Proofview.Goal.enter begin fun gl ->
-      let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
-      let freshn = fresh_id (Id.of_string "x") gl in
-      let freshm = fresh_id (Id.of_string "y") gl in
-      let freshz = fresh_id (Id.of_string "Z") gl in
-  (* try with *)
-      Tacticals.New.tclTHENLIST [ intros_using fresh_first_intros;
-                     intro_using freshn ;
-                     induct_on (EConstr.mkVar freshn);
-                     intro_using freshm;
-                     destruct_on (EConstr.mkVar freshm);
-                     intro_using freshz;
-                     intros;
-                     Tacticals.New.tclTRY (
-                      Tacticals.New.tclORELSE reflexivity my_discr_tac
-                     );
-                     my_inj_tac freshz;
-                     intros; simpl_in_concl;
-                     Auto.default_auto;
-                     Tacticals.New.tclREPEAT (
-                      Tacticals.New.tclTHENLIST [apply (EConstr.of_constr (andb_true_intro()));
-                                  simplest_split ;Auto.default_auto ]
-                      );
-                      Proofview.Goal.enter begin fun gls ->
-                        let concl = Proofview.Goal.concl gls in
-                        let sigma = Tacmach.New.project gl in
-                        (* assume the goal to be eq (eq_type ...) = true *)
-                        match EConstr.kind sigma concl with
-                        | App(c,ca) -> (match (EConstr.kind sigma ca.(1)) with
-                          | App(c',ca') ->
-                              let n = Array.length ca' in
-                              do_replace_lb mode lb_scheme_key
-                                (!avoid)
-                                nparrec
-                                ca'.(n-2) ca'.(n-1)
-                          | _ ->
-                              Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.")
-                        )
-                        | _ ->
-                            Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.")
-                      end
-                    ]
-      end
+  let first_intros =
+    ( List.map (fun (s,_,_,_) -> s ) list_id )
+    @ ( List.map (fun (_,seq,_,_) -> seq) list_id )
+    @ ( List.map (fun (_,_,_,slb) -> slb) list_id )
+  in
+  intros_using_then first_intros begin fun fresh_first_intros ->
+    Tacticals.New.tclTHENLIST [
+        intro_using_then (Id.of_string "x") (fun freshn -> induct_on (EConstr.mkVar freshn));
+        intro_using_then (Id.of_string "y") (fun freshm -> destruct_on (EConstr.mkVar freshm));
+        intro_using_then (Id.of_string "Z") begin fun freshz ->
+          Tacticals.New.tclTHENLIST [
+              intros;
+              Tacticals.New.tclTRY (
+                  Tacticals.New.tclORELSE reflexivity my_discr_tac
+                );
+              my_inj_tac freshz;
+              intros; simpl_in_concl;
+              Auto.default_auto;
+              Tacticals.New.tclREPEAT (
+                  Tacticals.New.tclTHENLIST [apply (EConstr.of_constr (andb_true_intro()));
+                                             simplest_split ;Auto.default_auto ]
+                );
+              Proofview.Goal.enter begin fun gls ->
+                let concl = Proofview.Goal.concl gls in
+                let sigma = Tacmach.New.project gls in
+                (* assume the goal to be eq (eq_type ...) = true *)
+                match EConstr.kind sigma concl with
+                | App(c,ca) -> (match (EConstr.kind sigma ca.(1)) with
+                                | App(c',ca') ->
+                                   let n = Array.length ca' in
+                                   do_replace_lb mode lb_scheme_key
+                                     (List.rev fresh_first_intros)
+                                     nparrec
+                                     ca'.(n-2) ca'.(n-1)
+                                | _ ->
+                                   Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.")
+                               )
+                | _ ->
+                   Tacticals.New.tclZEROMSG (str "Failure while solving Leibniz->Boolean.")
+                end
+            ]
+          end
+      ]
+    end
 
 let lb_scheme_kind_aux = ref (fun () -> failwith "Undefined")
 
@@ -868,10 +849,10 @@ let compute_dec_goal ind lnamesparrec nparrec =
   check_not_is_defined ();
   let eq = eq () and tt = tt () and bb = bb () in
   let list_id = list_id lnamesparrec in
-  let avoid = List.fold_right (Nameops.Name.fold_right (fun id l -> Id.Set.add id l)) (List.map RelDecl.get_name lnamesparrec) Id.Set.empty in
+  let avoid = avoid_of_list_id list_id in
+  let x = next_ident_away (Id.of_string "x") avoid in
+  let y = next_ident_away (Id.of_string "y") (Id.Set.add x avoid) in
     let create_input c =
-      let x = next_ident_away (Id.of_string "x") avoid and
-          y = next_ident_away (Id.of_string "y") avoid in
       let lb_typ = List.map (fun (s,seq,_,_) ->
         mkNamedProd (make_annot x Sorts.Relevant) (mkVar s) (
             mkNamedProd (make_annot y Sorts.Relevant) (mkVar s) (
@@ -912,12 +893,10 @@ let compute_dec_goal ind lnamesparrec nparrec =
           in
           mkNamedProd x (RelDecl.get_type decl) a) eq_input lnamesparrec
     in
-      let n = next_ident_away (Id.of_string "x") avoid and
-          m = next_ident_away (Id.of_string "y") avoid in
-        let eqnm = mkApp(eq,[|mkFullInd ind (2*nparrec+2);mkVar n;mkVar m|]) in
+        let eqnm = mkApp(eq,[|mkFullInd ind (2*nparrec+2);mkVar x;mkVar y|]) in
         create_input (
-          mkNamedProd (make_annot n Sorts.Relevant) (mkFullInd ind (2*nparrec)) (
-            mkNamedProd (make_annot m Sorts.Relevant) (mkFullInd ind (2*nparrec+1)) (
+          mkNamedProd (make_annot x Sorts.Relevant) (mkFullInd ind (2*nparrec)) (
+            mkNamedProd (make_annot y Sorts.Relevant) (mkFullInd ind (2*nparrec+1)) (
               mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_monomorphic_global @@ Coqlib.lib_ref "core.not.type",[|eqnm|])|])
           )
         )
@@ -925,83 +904,89 @@ let compute_dec_goal ind lnamesparrec nparrec =
 
 let compute_dec_tact ind lnamesparrec nparrec =
   let eq = eq () and tt = tt ()
-  and ff = ff () and bb = bb () in
+      and ff = ff () and bb = bb () in
   let list_id = list_id lnamesparrec in
   find_scheme beq_scheme_kind ind >>= fun _ ->
-  let eqI = eqI ind lnamesparrec in
-  let avoid = ref [] in
+  let _non_fresh_eqI = eqI ind list_id in
   let eqtrue x = mkApp(eq,[|bb;x;tt|]) in
   let eqfalse x = mkApp(eq,[|bb;x;ff|]) in
   let first_intros =
-      ( List.map (fun (s,_,_,_) -> s ) list_id ) @
-      ( List.map (fun (_,seq,_,_) -> seq) list_id ) @
-      ( List.map (fun (_,_,sbl,_) -> sbl) list_id ) @
-      ( List.map (fun (_,_,_,slb) -> slb) list_id )
-  in
-  let fresh_id s gl =
-      let fresh = fresh_id_in_env (Id.Set.of_list !avoid) s (Proofview.Goal.env gl) in
-      avoid := fresh::(!avoid); fresh
+    ( List.map (fun (s,_,_,_) -> s ) list_id )
+    @ ( List.map (fun (_,seq,_,_) -> seq) list_id )
+    @ ( List.map (fun (_,_,sbl,_) -> sbl) list_id )
+    @ ( List.map (fun (_,_,_,slb) -> slb) list_id )
   in
-  Proofview.Goal.enter begin fun gl ->
-  let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
-  let freshn = fresh_id (Id.of_string "x") gl in
-  let freshm = fresh_id (Id.of_string "y") gl in
-  let freshH = fresh_id (Id.of_string "H") gl in
-  let eqbnm = mkApp(eqI,[|mkVar freshn;mkVar freshm|]) in
-  let arfresh = Array.of_list fresh_first_intros in
-  let xargs = Array.sub arfresh 0 (2*nparrec) in
-  find_scheme bl_scheme_kind ind >>= fun c ->
-  let blI = mkConst c in
-  find_scheme lb_scheme_kind ind >>= fun c ->
-  let lbI = mkConst c in
-  Tacticals.New.tclTHENLIST [
-        intros_using fresh_first_intros;
-        intros_using [freshn;freshm];
-        (*we do this so we don't have to prove the same goal twice *)
-        assert_by (Name freshH) (EConstr.of_constr (
-          mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|])
-        ))
-          (Tacticals.New.tclTHEN (destruct_on (EConstr.of_constr eqbnm)) Auto.default_auto);
-
+  let fresh_id s gl = fresh_id_in_env (Id.Set.empty) s (Proofview.Goal.env gl) in
+  intros_using_then first_intros begin fun fresh_first_intros ->
+    let eqI =
+      let a = Array.of_list fresh_first_intros in
+      let n = List.length list_id in
+      assert (Int.equal (Array.length a) (4 * n));
+      let fresh_list_id =
+        List.init n (fun i -> (Array.get a i, Array.get a (i+n),
+                               Array.get a (i+2*n), Array.get a (i+3*n))) in
+      eqI ind fresh_list_id
+    in
+    intro_using_then (Id.of_string "x") begin fun freshn ->
+      intro_using_then (Id.of_string "y") begin fun freshm ->
         Proofview.Goal.enter begin fun gl ->
-          let freshH2 = fresh_id (Id.of_string "H") gl in
-          Tacticals.New.tclTHENS (destruct_on_using (EConstr.mkVar freshH) freshH2) [
-            (* left *)
-            Tacticals.New.tclTHENLIST [
-              simplest_left;
-              apply (EConstr.of_constr (mkApp(blI,Array.map mkVar xargs)));
-              Auto.default_auto
-            ]
-            ;
-
-            (*right *)
-            Proofview.Goal.enter begin fun gl ->
-            let freshH3 = fresh_id (Id.of_string "H") gl in
-            Tacticals.New.tclTHENLIST [
-              simplest_right ;
-              unfold_constr (Coqlib.lib_ref "core.not.type");
-              intro;
-              Equality.subst_all ();
-              assert_by (Name freshH3)
-                (EConstr.of_constr (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|])))
-                (Tacticals.New.tclTHENLIST [
-                  apply (EConstr.of_constr (mkApp(lbI,Array.map mkVar xargs)));
-                  Auto.default_auto
-                ]);
-              Equality.general_rewrite_bindings_in true
-                              Locus.AllOccurrences true false
-                              (List.hd !avoid)
-                              ((EConstr.mkVar (List.hd (List.tl !avoid))),
-                                NoBindings
-                              )
-                              true;
-              my_discr_tac
+          let freshH = fresh_id (Id.of_string "H") gl in
+          let eqbnm = mkApp(eqI,[|mkVar freshn;mkVar freshm|]) in
+          let arfresh = Array.of_list fresh_first_intros in
+          let xargs = Array.sub arfresh 0 (2*nparrec) in
+          find_scheme bl_scheme_kind ind >>= fun c ->
+          let blI = mkConst c in
+          find_scheme lb_scheme_kind ind >>= fun c ->
+          let lbI = mkConst c in
+          Tacticals.New.tclTHENLIST [
+              (*we do this so we don't have to prove the same goal twice *)
+              assert_by (Name freshH) (EConstr.of_constr (
+                                           mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|])
+                ))
+                (Tacticals.New.tclTHEN (destruct_on (EConstr.of_constr eqbnm)) Auto.default_auto);
+
+              Proofview.Goal.enter begin fun gl ->
+                let freshH2 = fresh_id (Id.of_string "H") gl in
+                Tacticals.New.tclTHENS (destruct_on_using (EConstr.mkVar freshH) freshH2) [
+                    (* left *)
+                    Tacticals.New.tclTHENLIST [
+                        simplest_left;
+                        apply (EConstr.of_constr (mkApp(blI,Array.map mkVar xargs)));
+                        Auto.default_auto
+                      ]
+                  ;
+
+                    (*right *)
+                    Proofview.Goal.enter begin fun gl ->
+                      let freshH3 = fresh_id (Id.of_string "H") gl in
+                      Tacticals.New.tclTHENLIST [
+                          simplest_right ;
+                          unfold_constr (Coqlib.lib_ref "core.not.type");
+                          intro;
+                          Equality.subst_all ();
+                          assert_by (Name freshH3)
+                            (EConstr.of_constr (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|])))
+                            (Tacticals.New.tclTHENLIST [
+                                 apply (EConstr.of_constr (mkApp(lbI,Array.map mkVar xargs)));
+                                 Auto.default_auto
+                            ]);
+                          Equality.general_rewrite_bindings_in true
+                            Locus.AllOccurrences true false
+                            freshH3
+                            ((EConstr.mkVar freshH2),
+                             NoBindings
+                            )
+                            true;
+                          my_discr_tac
+                        ]
+                      end
+                  ]
+                end
             ]
-            end
-          ]
+          end
         end
-  ]
-  end
+      end
+    end
 
 let make_eq_decidability mode mind =
   let mib = Global.lookup_mind mind in