aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2996.v
blob: d5409289c5c3bdb92e13e0ebabbc30a659d385f5 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
Require Import TestSuite.admit.
(* 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.