Get rid of "shouldsucceed" subdirectory by moving tests to parent directory.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16797 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 28 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/1448.v b/test-suite/bugs/closed/1448.v
new file mode 100644
index 000000000..fe3b4c8b4
--- /dev/null
+++ b/test-suite/bugs/closed/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).