Imported Upstream version 8.5~beta1+dfsg

1 files changed, 30 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/2996.v b/test-suite/bugs/closed/2996.v
new file mode 100644
index 00000000..440cda61
--- /dev/null
+++ b/test-suite/bugs/closed/2996.v
@@ -0,0 +1,30 @@
+(* Test on definitions referring to section variables that are not any
+   longer in the current context *)
+
+Section x.
+
+  Hypothesis h : forall(n : nat), n < S n.
+
+  Definition f(n m : nat)(less : n < m) : nat := n + m.
+
+  Lemma a : forall(n : nat), f n (S n) (h n) = 1 + 2 * n.
+  Proof.
+    (* XXX *) admit.
+  Qed.
+
+  Lemma b : forall(n : nat), n < 3 + n.
+  Proof.
+    clear.
+    intros n.
+    Fail assert (H := a n).
+  Abort.
+
+  Let T := True.
+  Definition p := I : T.
+
+  Lemma paradox : False.
+  Proof.
+    clear.
+    set (T := False).
+    Fail pose proof p as H.
+  Abort.