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
|
Set Implicit Arguments.
Unset Strict Implicit.
Module OK.
Record A := mkA {
T : Type;
P : T -> bool;
}.
About P. (* Argument a is implicit *)
Check P (true: T (mkA negb)).
End OK.
Module KO.
Set Primitive Projections.
Record A := mkA {
T : Type;
P : T -> bool;
}.
About P. (* No implicit arguments *)
Check P (true: T (mkA negb)).
(*
The command has indeed failed with message:
The term "true : T {| T := bool; P := negb |}" has type "T {| T := bool; P := negb |}"
while it is expected to have type "A".
*)
End KO.
|
