Imported Upstream version 8.5~beta1+dfsg

1 files changed, 0 insertions, 28 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/1448.v b/test-suite/bugs/closed/shouldsucceed/1448.v
deleted file mode 100644
index fe3b4c8b..00000000
--- a/test-suite/bugs/closed/shouldsucceed/1448.v
+++ /dev/null
@@ -1,28 +0,0 @@
-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).