4 files changed, 18 insertions, 15 deletions
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index a9f9c805d8..1e9be8dded 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -396,8 +396,8 @@ operconstr0: [
 (* @Zimmi48: This rule is a hack, according to Hugo, and should not be shown in the manual. *)
 | DELETE "{" binder_constr "}"
 | REPLACE "{|" record_declaration bar_cbrace
-| WITH "{|" LIST0 field_def bar_cbrace
-| MOVETO term_record "{|" LIST0 field_def bar_cbrace
+| WITH "{|" LIST0 field_def SEP ";" OPT ";" bar_cbrace
+| MOVETO term_record "{|" LIST0 field_def SEP ";" OPT ";" bar_cbrace
 | MOVETO term_generalizing "`{" operconstr200 "}"
 | MOVETO term_generalizing "`(" operconstr200 ")"
 | MOVETO term_ltac "ltac" ":" "(" tactic_expr5 ")"
@@ -585,7 +585,7 @@ constructor_list_or_record_decl: [
 
 record_fields: [
 | REPLACE record_field ";" record_fields
-| WITH LIST0 record_field SEP ";"
+| WITH LIST0 record_field SEP ";" OPT ";"
 | DELETE record_field
 | DELETE (* empty *)
 ]
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml
index 0ac652c0db..177abe53fc 100644
--- a/doc/tools/docgram/doc_grammar.ml
+++ b/doc/tools/docgram/doc_grammar.ml
@@ -909,14 +909,17 @@ let apply_splice g edit_map =
   List.iter (fun b ->
       let (nt0, prods0) = b in
       let rec splice_loop nt prods cnt =
-        let max_cnt = 10 in
-        let (nt', prods') = edit_rule g edit_map nt prods in
-        if cnt > max_cnt then
-          error "Splice for '%s' not done after %d iterations\n" nt0 max_cnt;
-        if nt' = nt && prods' = prods then
-          (nt', prods')
-        else
-          splice_loop nt' prods' (cnt+1)
+        if cnt >= 10 then begin
+          error "Splice for '%s' not done after %d iterations.  Current value is:\n" nt0 cnt;
+          List.iter (fun prod -> Printf.eprintf "  %s\n" (prod_to_str prod)) prods;
+          (nt, prods)
+        end else begin
+          let (nt', prods') = edit_rule g edit_map nt prods in
+          if nt' = nt && prods' = prods then
+            (nt, prods)
+          else
+            splice_loop nt' prods' (cnt+1)
+        end
       in
       let (nt', prods') = splice_loop nt0 prods0 0 in
       g_update_prods g nt' prods')
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 067050b4f5..73641976e3 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1740,11 +1740,11 @@ simple_tactic: [
 | "zify_elim_let"      (* micromega plugin *)
 | "nsatz_compute" constr      (* nsatz plugin *)
 | "omega"      (* omega plugin *)
-| "rtauto"
 | "protect_fv" string "in" ident      (* ring plugin *)
 | "protect_fv" string      (* ring plugin *)
 | "ring_lookup" tactic0 "[" LIST0 constr "]" LIST1 constr      (* ring plugin *)
 | "field_lookup" tactic "[" LIST0 constr "]" LIST1 constr      (* ring plugin *)
+| "rtauto"
 ]
 
 mlname: [
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index cbef29fb39..61befe9f1f 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -539,7 +539,7 @@ variant_definition: [
 ]
 
 record_definition: [
-| OPT ">" ident_decl LIST0 binder OPT [ ":" type ] OPT ident "{" LIST0 record_field SEP ";" "}" OPT decl_notations
+| OPT ">" ident_decl LIST0 binder OPT [ ":" type ] OPT ident "{" LIST0 record_field SEP ";" OPT ";" "}" OPT decl_notations
 ]
 
 record_field: [
@@ -553,7 +553,7 @@ field_body: [
 ]
 
 term_record: [
-| "{|" LIST0 field_def "|}"
+| "{|" LIST0 field_def SEP ";" OPT ";" "|}"
 ]
 
 field_def: [
@@ -566,7 +566,7 @@ inductive_definition: [
 
 constructors_or_record: [
 | OPT "|" LIST1 constructor SEP "|"
-| OPT ident "{" LIST0 record_field SEP ";" "}"
+| OPT ident "{" LIST0 record_field SEP ";" OPT ";" "}"
 ]
 
 constructor: [