1 files changed, 0 insertions, 27 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/808_2411.v b/test-suite/bugs/closed/shouldsucceed/808_2411.v
deleted file mode 100644
index 1c13e745..00000000
--- a/test-suite/bugs/closed/shouldsucceed/808_2411.v
+++ /dev/null
@@ -1,27 +0,0 @@
-Section test.
-Variable n:nat.
-Lemma foo: 0 <= n.
-Proof.
-(* declaring an Axiom during a proof makes it immediatly
-   usable, juste as a full Definition. *)
-Axiom bar : n = 1.
-rewrite bar.
-now apply le_S.
-Qed.
-
-Lemma foo' : 0 <= n.
-Proof.
-(* Declaring an Hypothesis during a proof is ok,
-   but this hypothesis won't be usable by the current proof(s),
-   only by later ones. *)
-Hypothesis bar' : n = 1.
-Fail rewrite bar'.
-Abort.
-
-Lemma foo'' : 0 <= n.
-Proof.
-rewrite bar'.
-now apply le_S.
-Qed.
-
-End test.
-\ No newline at end of file