blob: c9b50913472f91f537e161b7ac532ace351285b7 (
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
|
(* Test error messages *)
(* Test non-regression of bug fixed in r13486 (bad printer for module names) *)
Module Type S.
Parameter t:Type.
End S.
Module M : S.
Fail End M.
(* A simple check of how Ltac trace are used or not *)
(* Unfortunately, cannot test error location... *)
Ltac f x := apply x.
Goal True.
Fail simpl; apply 0.
Fail simpl; f 0.
Abort.
(* Test instantiate error messages *)
Goal forall T1 (P1 : T1 -> Type), sigT P1 -> sigT P1.
intros T1 P1 H1.
eexists ?[x].
destruct H1 as [x1 H1].
Fail instantiate (x:=projT1 x1).
Abort.
(* Test some messages for non solvable evars *)
Fail Goal forall a f, f a = 0.
Fail Goal forall f x, id f x = 0.
Fail Goal forall f P, P (f 0).
|
