ring: generate fresh names for lemmas

Fix #12889

2 files changed, 41 insertions, 9 deletions

diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 95faede7d0..6ed6b8da91 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -146,17 +146,21 @@ let ic_unsafe c = (*FIXME remove *)
   let sigma = Evd.from_env env in
   fst (Constrintern.interp_constr env sigma c)
 
-let decl_constant na univs c =
+let decl_constant name univs c =
   let open Constr in
   let vars = CVars.universes_of_constr c in
   let univs = UState.restrict_universe_context ~lbound:(Global.universes_lbound ()) univs vars in
   let () = DeclareUctx.declare_universe_context ~poly:false univs in
   let types = (Typeops.infer (Global.env ()) c).uj_type in
   let univs = Monomorphic_entry Univ.ContextSet.empty in
-  mkConst(declare_constant ~name:(Id.of_string na)
+  mkConst(declare_constant ~name
             ~kind:Decls.(IsProof Lemma)
             (DefinitionEntry (definition_entry ~opaque:true ~types ~univs c)))
 
+let decl_constant na suff univs c =
+  let na = Namegen.next_global_ident_away (Nameops.add_suffix na suff) Id.Set.empty in
+  decl_constant na univs c
+
 (* Calling a global tactic *)
 let ltac_call tac (args:glob_tactic_arg list) =
   TacArg(CAst.make @@ TacCall (CAst.make (ArgArg(Loc.tag @@ Lazy.force tac),args)))
@@ -581,9 +585,9 @@ let add_theory0 name (sigma, rth) eqth morphth cst_tac (pre,post) power sign div
   let lemma2 = params.(4) in
 
   let lemma1 =
-    decl_constant (Id.to_string name^"_ring_lemma1") ctx lemma1 in
+    decl_constant name "_ring_lemma1" ctx lemma1 in
   let lemma2 =
-    decl_constant (Id.to_string name^"_ring_lemma2") ctx lemma2 in
+    decl_constant name "_ring_lemma2" ctx lemma2 in
   let cst_tac =
     interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
   let pretac =
@@ -898,15 +902,15 @@ let add_field_theory0 name fth eqth morphth cst_tac inj (pre,post) power sign od
     match inj with
       | Some thm -> mkApp(params.(8),[|EConstr.to_constr sigma thm|])
       | None -> params.(7) in
-  let lemma1 = decl_constant (Id.to_string name^"_field_lemma1")
+  let lemma1 = decl_constant name "_field_lemma1"
     ctx lemma1 in
-  let lemma2 = decl_constant (Id.to_string name^"_field_lemma2")
+  let lemma2 = decl_constant name "_field_lemma2"
     ctx lemma2 in
-  let lemma3 = decl_constant (Id.to_string name^"_field_lemma3")
+  let lemma3 = decl_constant name "_field_lemma3"
     ctx lemma3 in
-  let lemma4 = decl_constant (Id.to_string name^"_field_lemma4")
+  let lemma4 = decl_constant name "_field_lemma4"
     ctx lemma4 in
-  let cond_lemma = decl_constant (Id.to_string name^"_lemma5")
+  let cond_lemma = decl_constant name "_lemma5"
     ctx cond_lemma in
   let cst_tac =
     interp_cst_tac env sigma morphth kind (zero,one,add,mul,opp) cst_tac in
diff --git a/test-suite/bugs/closed/bug_12889.v b/test-suite/bugs/closed/bug_12889.v
new file mode 100644
index 0000000000..f53cb8272d
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12889.v
@@ -0,0 +1,28 @@
+Require Import Relations.
+Require Import Setoid.
+Require Import Ring_theory.
+Require Import Ring_base.
+
+Section S1.
+Variable R : Type.
+Variable Rone Rzero : R.
+Variable Rplus Rmult Rminus : R -> R -> R.
+Variable Rneg : R -> R.
+
+Lemma my_ring_theory1 : @ring_theory R Rzero Rone Rplus Rmult Rminus Rneg (@eq
+R).
+Admitted.
+Add Ring my_ring : my_ring_theory1.
+End S1.
+
+Section S2.
+Variable R : Type.
+Variable Rone Rzero : R.
+Variable Rplus Rmult Rminus : R -> R -> R.
+Variable Rneg : R -> R.
+
+Lemma my_ring_theory2 : @ring_theory R Rzero Rone Rplus Rmult Rminus Rneg (@eq
+R).
+Admitted.
+Add Ring my_ring : my_ring_theory2.
+End S2.