Imported Upstream version 8.5~beta1+dfsg

1 files changed, 0 insertions, 20 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/1643.v b/test-suite/bugs/closed/shouldsucceed/1643.v
deleted file mode 100644
index 879a65b1..00000000
--- a/test-suite/bugs/closed/shouldsucceed/1643.v
+++ /dev/null
@@ -1,20 +0,0 @@
-(* Check some aspects of that the algorithm used to possibly reuse a
-   global name in the recursive calls (coinductive case) *)
-
-CoInductive Str : Set := Cons (h:nat) (t:Str).
-
-Definition decomp_func (s:Str) :=
-  match s with
-    | Cons h t => Cons h t
-  end.
-
-Theorem decomp s: s = decomp_func s.
-Proof.
-  case s; simpl; reflexivity.
-Qed.
-
-Definition zeros := (cofix z : Str := Cons 0 z).
-Lemma zeros_rw : zeros = Cons 0 zeros.
-  rewrite (decomp zeros).
-  simpl.
-Admitted.