blob: fbd9c8bcbac3a45e3a31f8d637fb4328af9b30f7 (
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
|
Module TestUnsetTemplateCheck.
Unset Template Check.
Section Foo.
Context (A : Type).
Definition cstr := nat : ltac:(let ty := type of A in exact ty).
Inductive myind :=
| cons : A -> myind.
End Foo.
(* Can only succeed if no template check is performed *)
Check myind True : Prop.
About myind.
(* test discharge puts things in the right order (by using the
checker on the result) *)
Section S.
Variables (A:Type) (a:A).
Inductive bb (B:Type) := BB : forall a', a = a' -> B -> bb B.
End S.
End TestUnsetTemplateCheck.
|
