From 53e7cfdbece60e775c2b421050ef825c4a8c9d50 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 15 Sep 2011 15:03:32 +0000 Subject: Re-allowing assumptions during proofs seems safe now (fix #2411) This restriction was introduce to solve #808, whose underlying issue (causing a anomaly) doesn't seem active anymore. Semantic: - Axiom in the middle of a proof : immediatly usable (just as a Definition) - Hypothesis or Variable : not visible in current proof, only usable in the next ones. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14470 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/bugs/closed/shouldsucceed/808_2411.v | 27 +++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 test-suite/bugs/closed/shouldsucceed/808_2411.v (limited to 'test-suite/bugs/closed') diff --git a/test-suite/bugs/closed/shouldsucceed/808_2411.v b/test-suite/bugs/closed/shouldsucceed/808_2411.v new file mode 100644 index 000000000..1c13e7454 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/808_2411.v @@ -0,0 +1,27 @@ +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 -- cgit v1.2.3