Use properly fresh names for Scheme Equality

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 =

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
 

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.