Record fields accept an optional final semicolon separator.

There is no such thing as the OPTSEP macro in Camlp4 so I had
to expand it by hand.

2 files changed, 28 insertions, 5 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 9fe302234..e2e6795f7 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -224,11 +224,20 @@ GEXTEND Gram
       ] ]
   ;
   record_declaration:
-    [ [ fs = LIST0 record_field_declaration SEP ";" -> CRecord (!@loc, None, fs)
+    [ [ fs = record_fields -> CRecord (!@loc, None, fs)
 (*       | c = lconstr; "with"; fs = LIST1 record_field_declaration SEP ";" -> *)
 (* 	  CRecord (!@loc, Some c, fs) *)
     ] ]
   ;
+
+  record_fields:
+    [ [ f = record_field_declaration; ";"; fs = record_fields -> f :: fs
+      | f = record_field_declaration; ";" -> [f]
+      | f = record_field_declaration -> [f]
+      | -> []
+    ] ]
+  ;
+
   record_field_declaration:
     [ [ id = global; params = LIST0 identref; ":="; c = lconstr ->
       (id, abstract_constr_expr c (binders_of_lidents params)) ] ]
@@ -356,9 +365,16 @@ GEXTEND Gram
     [ [ pll = LIST1 mult_pattern SEP "|";
         "=>"; rhs = lconstr -> (!@loc,pll,rhs) ] ]
   ;
-  recordpattern:
+  record_pattern:
     [ [ id = global; ":="; pat = pattern -> (id, pat) ] ]
   ;
+  record_patterns:
+    [ [ p = record_pattern; ";"; ps = record_patterns -> p :: ps
+      | p = record_pattern; ";" -> [p]
+      | p = record_pattern-> [p]
+      | -> []
+    ] ]
+  ;
   pattern:
     [ "200" RIGHTA [ ]
     | "100" RIGHTA
@@ -382,7 +398,7 @@ GEXTEND Gram
       [ c = pattern; "%"; key=IDENT -> CPatDelimiters (!@loc,key,c) ]
     | "0"
       [ r = Prim.reference -> CPatAtom (!@loc,Some r)
-      | "{|"; pat = LIST0 recordpattern SEP ";" ; "|}" -> CPatRecord (!@loc, pat)
+      | "{|"; pat = record_patterns; "|}" -> CPatRecord (!@loc, pat)
       | "_" -> CPatAtom (!@loc,None)
       | "("; p = pattern LEVEL "200"; ")" ->
           (match p with
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 63850713f..e9915fceb 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -325,9 +325,9 @@ GEXTEND Gram
       | id = identref ; c = constructor_type; "|"; l = LIST0 constructor SEP "|" ->
 	  Constructors ((c id)::l)
       | id = identref ; c = constructor_type -> Constructors [ c id ]
-      | cstr = identref; "{"; fs = LIST0 record_field SEP ";"; "}" ->
+      | cstr = identref; "{"; fs = record_fields; "}" ->
 	  RecordDecl (Some cstr,fs)
-      | "{";fs = LIST0 record_field SEP ";"; "}" -> RecordDecl (None,fs)
+      | "{";fs = record_fields; "}" -> RecordDecl (None,fs)
       |  -> Constructors [] ] ]
   ;
 (*
@@ -389,6 +389,13 @@ GEXTEND Gram
   [ [ bd = record_binder; pri = OPT [ "|"; n = natural -> n ];
       ntn = decl_notation -> (bd,pri),ntn ] ]
   ;
+  record_fields:
+    [ [ f = record_field; ";"; fs = record_fields -> f :: fs
+      | f = record_field; ";" -> [f]
+      | f = record_field -> [f]
+      | -> []
+    ] ]
+  ;
   record_binder_body:
     [ [ l = binders; oc = of_type_with_opt_coercion;
          t = lconstr -> fun id -> (oc,AssumExpr (id,mkCProdN (!@loc) l t))