diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/bug_12889.v | 28 |
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. |