Use fresher names in eqschemes.

The previous implementation appears to be sound when Mangle Names is
off, but it relies on two fragile assumptions, namely that
next_global_ident_away always returns different identifiers when called
with naming hints which are different after stripping all digits from
the end, and that default_id_of_sort (locally defined) never returns
"HC" or "P", or either of those followed by a string of digits.

These changes make both assumptions unnecessary.

As a side note, it seems odd that fresh is ignoring it's env parameter.

2 files changed, 26 insertions, 15 deletions

diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 955a7957bf..f90c143a1a 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -68,7 +68,9 @@ module RelDecl = Context.Rel.Declaration
 let hid = Id.of_string "H"
 let xid = Id.of_string "X"
 let default_id_of_sort = function InSProp | InProp | InSet -> hid | InType -> xid
-let fresh env id = next_global_ident_away id Id.Set.empty
+let fresh env id avoid =
+  let freshid = next_global_ident_away id avoid in
+  freshid, Id.Set.add freshid avoid
 let with_context_set ctx (b, ctx') =
   (b, Univ.ContextSet.union ctx ctx')
 
@@ -204,7 +206,7 @@ let build_sym_scheme env ind =
   let cstr n =
     mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect mkRel n mib.mind_params_ctxt) in
   let inds = snd (mind_arity mip) in
-  let varH = fresh env (default_id_of_sort inds) in
+  let varH,_ = fresh env (default_id_of_sort inds) Id.Set.empty in
   let applied_ind = build_dependent_inductive indu specif in
   let indr = Sorts.relevance_of_sort_family inds in
   let realsign_ind =
@@ -263,7 +265,7 @@ let build_sym_involutive_scheme env ind =
   let cstr n = mkApp (mkConstructUi (indu,1),Context.Rel.to_extended_vect mkRel n paramsctxt) in
   let inds = snd (mind_arity mip) in
   let indr = Sorts.relevance_of_sort_family inds in
-  let varH = fresh env (default_id_of_sort inds) in
+  let varH,_ = fresh env (default_id_of_sort inds) Id.Set.empty in
   let applied_ind = build_dependent_inductive indu specif in
   let applied_ind_C =
     mkApp
@@ -380,9 +382,9 @@ let build_l2r_rew_scheme dep env ind kind =
                     rel_vect p nrealargs]) in
   let inds = snd (mind_arity mip) in
   let indr = Sorts.relevance_of_sort_family inds in
-  let varH = fresh env (default_id_of_sort inds) in
-  let varHC = fresh env (Id.of_string "HC") in
-  let varP = fresh env (Id.of_string "P") in
+  let varH,avoid = fresh env (default_id_of_sort inds) Id.Set.empty in
+  let varHC,avoid = fresh env (Id.of_string "HC") avoid in
+  let varP,_ = fresh env (Id.of_string "P") avoid in
   let applied_ind = build_dependent_inductive indu specif in
   let applied_ind_P =
     mkApp (mkIndU indu, Array.concat
@@ -498,9 +500,9 @@ let build_l2r_forward_rew_scheme dep env ind kind =
                     rel_vect p nrealargs]) in
   let inds = snd (mind_arity mip) in
   let indr = Sorts.relevance_of_sort_family inds in
-  let varH = fresh env (default_id_of_sort inds) in
-  let varHC = fresh env (Id.of_string "HC") in
-  let varP = fresh env (Id.of_string "P") in
+  let varH,avoid = fresh env (default_id_of_sort inds) Id.Set.empty in
+  let varHC,avoid = fresh env (Id.of_string "HC") avoid in
+  let varP,_ = fresh env (Id.of_string "P") avoid in
   let applied_ind = build_dependent_inductive indu specif in
   let applied_ind_P =
     mkApp (mkIndU indu, Array.concat
@@ -593,9 +595,9 @@ let build_r2l_forward_rew_scheme dep env ind kind =
   let constrargs_cstr = constrargs@[cstr 0] in
   let inds = snd (mind_arity mip) in
   let indr = Sorts.relevance_of_sort_family inds in
-  let varH = fresh env (default_id_of_sort inds) in
-  let varHC = fresh env (Id.of_string "HC") in
-  let varP = fresh env (Id.of_string "P") in
+  let varH,avoid = fresh env (default_id_of_sort inds) Id.Set.empty in
+  let varHC,avoid = fresh env (Id.of_string "HC") avoid in
+  let varP,_ = fresh env (Id.of_string "P") avoid in
   let applied_ind = build_dependent_inductive indu specif in
   let realsign_ind =
     name_context env ((LocalAssum (make_annot (Name varH) indr,applied_ind))::realsign) in
@@ -806,9 +808,9 @@ let build_congr env (eq,refl,ctx) ind =
   if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then
     error "Constructor must have no arguments";
   let b = List.nth constrargs (i + mib.mind_nparams - 1) in
-  let varB = fresh env (Id.of_string "B") in
-  let varH = fresh env (Id.of_string "H") in
-  let varf = fresh env (Id.of_string "f") in
+  let varB,avoid = fresh env (Id.of_string "B") Id.Set.empty in
+  let varH,avoid = fresh env (Id.of_string "H") avoid in
+  let varf,avoid = fresh env (Id.of_string "f") avoid in
   let rci = Sorts.Relevant in (* TODO relevance *)
   let ci = make_case_info (Global.env()) ind rci RegularStyle in
   let uni, ctx = Univ.extend_in_context_set (UnivGen.new_global_univ ()) ctx in
diff --git a/test-suite/bugs/closed/bug_13003.v b/test-suite/bugs/closed/bug_13003.v
new file mode 100644
index 0000000000..570baef2ef
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13003.v
@@ -0,0 +1,9 @@
+Set Mangle Names.
+Import EqNotations.
+Lemma eq_sigT_sig_eq X P (x1 x2:X) H1 H2 :
+  forall (E1 : x1=x2), rew E1 in H1 = H2 -> existT P x1 H1 = existT P x2 H2.
+Proof.
+  intros ->.
+  intros <-.
+  reflexivity.
+Defined.