blob: 3241e1339bb7319188cb1d81591a75119181645a (
plain)
1
2
3
4
5
6
7
8
|
(* 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 in |- *.
Abort.
|
