aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/RecordFieldErrors.out
blob: 5b67f632c9b99ee4dfa6148306d1d4f504e625cf (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
The command has indeed failed with message:
unit: Not a projection.
The command has indeed failed with message:
unit: Not a projection.
The command has indeed failed with message:
This record contains fields of both t and t'.
The command has indeed failed with message:
unit: Not a projection.
The command has indeed failed with message:
This record defines several times the field foo.
The command has indeed failed with message:
This record defines several times the field unit.
The command has indeed failed with message:
unit: Not a projection of inductive t.