diff options
author | Siddharth Bhat <siddu.druid@gmail.com> | 2018-06-27 22:03:25 +0200 |
---|---|---|
committer | Siddharth Bhat <siddu.druid@gmail.com> | 2018-07-17 13:14:44 +0200 |
commit | 1300da19d13f7e46cf3a4b0b3396604ffc44a6d5 (patch) | |
tree | 577f1c1b6dbc64382a7623d77bc6e6756ed45a96 /test-suite/output/RecordMissingField.v | |
parent | b799252775563b4f46f5ea39cbfc469759e7a296 (diff) |
Change QuestionMark for better record field missing error message.
While we were adding a new field into `QuestionMark`, we
decided to go ahead and refactor the constructor to hold
an actual record. This record now holds the name, obligations, and
whether the evar represents a missing record field.
This is used to provide better error messages on missing record
fields.
Diffstat (limited to 'test-suite/output/RecordMissingField.v')
-rw-r--r-- | test-suite/output/RecordMissingField.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/test-suite/output/RecordMissingField.v b/test-suite/output/RecordMissingField.v new file mode 100644 index 000000000..84f1748fa --- /dev/null +++ b/test-suite/output/RecordMissingField.v @@ -0,0 +1,8 @@ +(** Check for error message when missing a record field. Error message +should contain missing field, and the inferred type of the record **) + +Record point2d := mkPoint { x2p: nat; y2p: nat }. + + +Definition increment_x (p: point2d) : point2d := + {| x2p := x2p p + 1; |}. |