From 2db5e308d06c4d5df9fb684cc214345a73f170e5 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 25 Aug 2020 10:59:54 +0200
Subject: ring: generate fresh names for lemmas

Fix #12889
---
 test-suite/bugs/closed/bug_12889.v | 28 ++++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_12889.v

(limited to 'test-suite')

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.
-- 
cgit v1.2.3