From 3a3d361e1fa3ce9a074789405f46ed4c1fc67b2f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 19 Nov 2019 21:01:41 +0100
Subject: G_constr: Renaming record_fields_instance -> fields_def.

This is in accordance with PR #10614 and to avoid a confusion with the
fields of a record type in g_vernac.ml.

Removing a useless line at the same time in G_vernac.
---
 parsing/g_constr.mlg | 10 +++++-----
 vernac/g_vernac.mlg  |  1 -
 2 files changed, 5 insertions(+), 6 deletions(-)

diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 3202cd3222..1cd36d2135 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -210,14 +210,14 @@ GRAMMAR EXTEND Gram
         { CAst.make ~loc @@ CGeneralization (Explicit, None, c) } ] ]
   ;
   record_declaration:
-    [ [ fs = record_fields_instance -> { CAst.make ~loc @@ CRecord fs } ] ]
+    [ [ fs = fields_def -> { CAst.make ~loc @@ CRecord fs } ] ]
   ;
-  record_fields_instance:
-    [ [ f = record_field_instance; ";"; fs = record_fields_instance -> { f :: fs }
-      | f = record_field_instance -> { [f] }
+  fields_def:
+    [ [ f = field_def; ";"; fs = fields_def -> { f :: fs }
+      | f = field_def -> { [f] }
       | -> { [] } ] ]
   ;
-  record_field_instance:
+  field_def:
     [ [ id = global; bl = binders; ":="; c = lconstr ->
         { (id, mkLambdaCN ~loc bl c) } ] ]
   ;
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index d534c107f1..61de1bfd26 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -488,7 +488,6 @@ GRAMMAR EXTEND Gram
   ;
   record_fields:
     [ [ f = record_field; ";"; fs = record_fields -> { f :: fs }
-      | f = record_field; ";" -> { [f] }
       | f = record_field -> { [f] }
       | -> { [] }
     ] ]
-- 
cgit v1.2.3