blob: b26a9ff1eb9019fcb45ef2a35190860360ec079a (
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
|
(* Testing remember and co *)
Lemma A : forall (P: forall X, X -> Prop), P nat 0 -> P nat 0.
intros.
Fail remember nat as X.
Fail remember nat as X in H. (* This line used to succeed in 8.3 *)
Fail remember nat as X.
Abort.
(* Testing Ltac interpretation of remember (was not working up to r16181) *)
Goal (1 + 2 + 3 = 6).
let name := fresh "fresh" in
remember (1 + 2) as x eqn:name.
rewrite fresh.
Abort.
(* An example which was working in 8.4 but failing in 8.5 and 8.5pl1 *)
Module A.
Axiom N : nat.
End A.
Module B.
Include A.
End B.
Goal id A.N = B.N.
reflexivity.
Qed.
|
