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.

1 files changed, 5 insertions, 5 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) } ] ]
   ;