Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 28 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/1448.v b/test-suite/bugs/closed/shouldsucceed/1448.v
new file mode 100644
index 00000000..fe3b4c8b
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1448.v
@@ -0,0 +1,28 @@
+Require Import Relations.
+Require Import Setoid.
+Require Import Ring_theory.
+Require Import Ring_base.
+
+
+Variable R : Type.
+Variable Rone Rzero : R.
+Variable Rplus Rmult Rminus : R -> R -> R.
+Variable Rneg : R -> R.
+
+Lemma my_ring_theory : @ring_theory R Rzero Rone Rplus Rmult Rminus Rneg (@eq
+R).
+Admitted.
+
+Variable Req : R -> R -> Prop.
+
+Hypothesis Req_refl : reflexive _ Req.
+Hypothesis Req_sym : symmetric _ Req.
+Hypothesis Req_trans : transitive _ Req.
+
+Add Relation R Req
+  reflexivity proved by Req_refl
+  symmetry proved by Req_sym
+  transitivity proved by Req_trans
+  as Req_rel.
+
+Add Ring my_ring : my_ring_theory (abstract).