diff options
| author | Hugo Herbelin | 2019-11-11 09:57:40 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-11-11 10:06:15 +0100 |
| commit | 1e5bae9d78192e3f0c5d7e25ab7e64fdc605316f (patch) | |
| tree | baabbbb92176e508d6a06bdda8fc10f5e396f9be | |
| parent | 69b91851ed5d18f1ca34ef2597f0cf342c10a124 (diff) | |
Miscellaneous improvements of the syntax of records.
- only one space instead of two when printing "{| |}"
- removing a redundant clause in the grammar of record_patterns
| -rw-r--r-- | parsing/g_constr.mlg | 1 | ||||
| -rw-r--r-- | printing/ppconstr.ml | 3 | ||||
| -rw-r--r-- | test-suite/output/Notations4.out | 2 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 7 |
4 files changed, 11 insertions, 2 deletions
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 470782a7dc..d377bd8561 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -393,7 +393,6 @@ GRAMMAR EXTEND Gram ; record_patterns: [ [ p = record_pattern; ";"; ps = record_patterns -> { p :: ps } - | p = record_pattern; ";" -> { [p] } | p = record_pattern-> { [p] } | -> { [] } ] ] diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 5ed96dd5e3..2da163b8ee 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -249,7 +249,8 @@ let tag_var = tag Tag.variable let pp (c, p) = pr_reference c ++ spc() ++ str ":=" ++ pr_patt spc (lpatrec, Any) p in - str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}", lpatrec + (if l = [] then str "{| |}" + else str "{| " ++ prlist_with_sep pr_semicolon pp l ++ str " |}"), lpatrec | CPatAlias (p, na) -> pr_patt mt (las,E) p ++ str " as " ++ pr_lname na, las diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index c1b9a2b1c6..ba4ac5a8f9 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -57,3 +57,5 @@ where |- Type] (pat, p0, p cannot be used) ?T0 : [y : nat pat : ?T0 * nat p0 : ?T0 * nat p := p0 : ?T0 * nat |- Type] (pat, p0, p cannot be used) +fun '{| |} => true + : R -> bool diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index d1063bfd04..4b9d0abd95 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -133,3 +133,10 @@ Check fun y : nat => # (x,z) |-> y & y. Check fun y : nat => # (x,z) |-> (x + y) & (y + z). End K. + +Module EmptyRecordSyntax. + +Record R := { n : nat }. +Check fun '{|n:=x|} => true. + +End EmptyRecordSyntax. |