blob: 22fb09526d9f21ad726c508bd619715a9c15e603 (
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
|
(* Test consistent behavior of Local Definition (#8722) *)
(* Test consistent behavior of Local Definition wrt Admitted *)
Module TestAdmittedVisibility.
Module A.
Let a1 : nat. Admitted. (* Suppose to behave like a "Local Definition" *)
Local Definition b1 : nat. Admitted. (* Told to be a "Local Definition" *)
Local Definition c1 := 0.
Local Parameter d1 : nat.
Section S.
Let a2 : nat. Admitted. (* Told to be turned into a toplevel assumption *)
Local Definition b2 : nat. Admitted. (* Told to be a "Local Definition" *)
Local Definition c2 := 0.
Local Parameter d2 : nat.
End S.
End A.
Import A.
Fail Check a1. (* used to be accepted *)
Fail Check b1. (* used to be accepted *)
Fail Check c1.
Fail Check d1.
Fail Check a2. (* used to be accepted *)
Fail Check b2. (* used to be accepted *)
Fail Check c2.
Fail Check d2.
End TestAdmittedVisibility.
(* Test consistent behavior of Local Definition wrt automatic declaration of instances *)
Module TestVariableAsInstances.
Module Test1.
Set Typeclasses Axioms Are Instances.
Class U.
Local Parameter b : U.
Definition testU := _ : U. (* _ resolved *)
Class T.
Variable a : T. (* warned to be the same as "Local Parameter" *)
Definition testT := _ : T. (* _ resolved *)
End Test1.
Module Test2.
Unset Typeclasses Axioms Are Instances.
Class U.
Local Parameter b : U.
Fail Definition testU := _ : U. (* _ unresolved *)
Class T.
Variable a : T. (* warned to be the same as "Local Parameter" thus should not be an instance *)
Fail Definition testT := _ : T. (* used to succeed *)
End Test2.
End TestVariableAsInstances.
|
