blob: b866c4b074187d1cff540a58068e3a6b17be9024 (
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
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
|
From Coq Require Program.Wf.
Section Scope.
#[local] Coercion nat_of_bool (b: bool) : nat :=
if b then 0 else 1.
Check (refl_equal : true = 0 :> nat).
End Scope.
Fail Check 0 = true :> nat.
#[universes(polymorphic)]
Definition ι T (x: T) := x.
Check ι _ ι.
#[universes(polymorphic=no)]
Definition ιι T (x: T) := x.
Fail Check ιι _ ιι.
#[program]
Fixpoint f (n: nat) {wf lt n} : nat := _.
Reset f.
#[program=yes]
Fixpoint f (n: nat) {wf lt n} : nat := _.
Reset f.
#[deprecated(since="8.9.0")]
Ltac foo := foo.
Module M.
#[local] #[universes(polymorphic)] Definition zed := Type.
#[local, universes(polymorphic)] Definition kats := Type.
End M.
Check M.zed@{_}.
Fail Check zed.
Check M.kats@{_}.
Fail Check kats.
Export Set Foo.
#[ export ] Set Foo.
Fail #[ export ] Export Foo.
(* Attribute for Locality specified twice *)
(* Tests for deprecated attribute syntax *)
Set Warnings "-deprecated-attribute-syntax".
#[program(true)]
Fixpoint f (n: nat) {wf lt n} : nat := _.
Reset f.
#[universes(monomorphic)]
Definition ιιι T (x: T) := x.
Fail Check ιιι _ ιιι.
|
