Merge PR #12890: ring: generate fresh names for lemmas

Reviewed-by: herbelin
Reviewed-by: maximedenes
Ack-by: SkySkimmer

1 files changed, 28 insertions, 0 deletions

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.