blob: fe7366a97d1e39d206398c698d8ffc45f1843cc9 (
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
32
33
34
35
36
37
38
|
(* Unification error tests *)
Module A.
(* Check regression of an UNBOUND_REL bug *)
Inductive T := C : forall {A}, A -> T.
Fail Check fun x => match x return ?[X] with C a => a end.
(* Bug #3634 *)
Fail Check (id:Type -> _).
End A.
(* Choice of evar names *)
Goal (forall x, S (S (S x)) = x) -> exists x, S x = 0.
eexists.
rewrite H.
Show.
Undo 2.
eexists ?[x].
rewrite H.
Show.
Undo 2.
eexists ?[y].
rewrite H.
Show.
reflexivity.
Qed.
(* Preserve the name if there is one *)
Goal (forall x, S x = x) -> exists x, S x = 0.
eexists ?[y].
rewrite H.
Show.
reflexivity.
Qed.
|
