blob: ff817c31aa1aeb7d78894f6058ecf1c705777ab3 (
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
|
(** Check that various errors in record fields are reported with the correct
underlying issue. *)
Record t :=
{ foo: unit }.
Record t' :=
{ bar: unit }.
Fail Check {| unit := tt |}.
(* unit: Not a projection. *)
Fail Check {| unit := tt;
foo := tt |}.
(* unit: Not a projection. *)
Fail Check {| foo := tt;
bar := tt |}.
(* This record contains fields of both t and t'. *)
Fail Check {| unit := tt;
unit := tt |}.
(* unit: Not a projection. *)
Fail Check {| foo := tt;
foo := tt |}.
(* This record defines several times the field foo. *)
Fail Check {| foo := tt;
unit := tt;
unit := tt |}.
(* This is slightly wrong (would prefer "unit: Not a projection."), but it's
acceptable and seems an unlikely mistake. *)
(* This record defines several times the field unit. *)
Fail Check {| foo := tt;
unit := tt |}.
(* unit: Not a projection. *)
|
