Merge PR #11079: Rename non-unique local nonterminals

Ack-by: Zimmi48
Ack-by: herbelin

4 files changed, 19 insertions, 21 deletions

diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index d377bd8561..b1d530438d 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -244,17 +244,17 @@ GRAMMAR EXTEND Gram
       ] ]
   ;
   record_declaration:
-    [ [ fs = record_fields -> { CAst.make ~loc @@ CRecord fs } ] ]
+    [ [ fs = record_fields_instance -> { CAst.make ~loc @@ CRecord fs } ] ]
   ;
 
-  record_fields:
-    [ [ f = record_field_declaration; ";"; fs = record_fields -> { f :: fs }
-      | f = record_field_declaration -> { [f] }
+  record_fields_instance:
+    [ [ f = record_field_instance; ";"; fs = record_fields_instance -> { f :: fs }
+      | f = record_field_instance -> { [f] }
       | -> { [] }
     ] ]
   ;
 
-  record_field_declaration:
+  record_field_instance:
     [ [ id = global; bl = binders; ":="; c = lconstr ->
       { (id, mkLambdaCN ~loc bl c) } ] ]
   ;
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 1b00a93834..eb282d1f83 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -439,7 +439,7 @@ GRAMMAR EXTEND Gram
     [ [ "in"; id = id_or_meta; ipat = as_ipat -> { Some (id,ipat) }
       | -> { None } ] ]
   ;
-  orient:
+  orient_rw:
     [ [ "->" -> { true }
       | "<-" -> { false }
       | -> { true } ] ]
@@ -451,10 +451,10 @@ GRAMMAR EXTEND Gram
     ] ]
   ;
   fixdecl:
-    [ [ "("; id = ident; bl=LIST0 simple_binder; ann=fixannot;
+    [ [ "("; id = ident; bl=LIST0 simple_binder; ann=struct_annot;
         ":"; ty=lconstr; ")" -> { (loc, id, bl, ann, ty) } ] ]
   ;
-  fixannot:
+  struct_annot:
     [ [ "{"; IDENT "struct"; id=name; "}" -> { Some id }
       | -> { None } ] ]
   ;
@@ -506,7 +506,7 @@ GRAMMAR EXTEND Gram
       ] ]
   ;
   oriented_rewriter :
-    [ [ b = orient; p = rewriter -> { let (m,c) = p in (b,m,c) } ] ]
+    [ [ b = orient_rw; p = rewriter -> { let (m,c) = p in (b,m,c) } ] ]
   ;
   induction_clause:
     [ [ c = destruction_arg; pat = as_or_and_ipat; eq = eqn_ipat;
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index cc3a7c0f79..c1bd585f3f 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -643,7 +643,7 @@ GRAMMAR EXTEND Gram
   q_conversion:
     [ [ c = conversion -> { c } ] ]
   ;
-  orient:
+  ltac2_orient:
     [ [ "->" -> { CAst.make ~loc (Some true) }
       | "<-" -> { CAst.make ~loc (Some false) }
       | -> { CAst.make ~loc None }
@@ -665,7 +665,7 @@ GRAMMAR EXTEND Gram
       ] ]
   ;
   oriented_rewriter:
-    [ [ b = orient; r = rewriter ->
+    [ [ b = ltac2_orient; r = rewriter ->
       { let (m, c) = r in
         CAst.make ~loc @@ {
         rew_orient = b;
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 4243d0c911..a78f4645c2 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -51,6 +51,7 @@ let decl_notation = Entry.create "vernac:decl_notation"
 let record_field = Entry.create "vernac:record_field"
 let of_type_with_opt_coercion = Entry.create "vernac:of_type_with_opt_coercion"
 let section_subset_expr = Entry.create "vernac:section_subset_expr"
+let scope_delimiter = Entry.create "vernac:scope_delimiter"
 
 let make_bullet s =
   let open Proof_bullet in
@@ -717,7 +718,7 @@ END
 
 (* Extensions: implicits, coercions, etc. *)
 GRAMMAR EXTEND Gram
-  GLOBAL: gallina_ext hint_info;
+  GLOBAL: gallina_ext hint_info scope_delimiter;
 
   gallina_ext:
     [ [ (* Transparent and Opaque *)
@@ -835,11 +836,11 @@ GRAMMAR EXTEND Gram
           { [`ClearImplicits; `ClearScopes] }
       ] ]
   ;
-  scope:
+  scope_delimiter:
     [ [ "%"; key = IDENT -> { key } ] ]
   ;
   argument_spec: [
-       [ b = OPT "!"; id = name ; s = OPT scope ->
+       [ b = OPT "!"; id = name ; s = OPT scope_delimiter ->
        { id.CAst.v, not (Option.is_empty b), Option.map (fun x -> CAst.make ~loc x) s }
     ]
   ];
@@ -852,7 +853,7 @@ GRAMMAR EXTEND Gram
              implicit_status = NotImplicit}] }
     | "/" -> { [`Slash] }
     | "&" -> { [`Ampersand] }
-    | "("; items = LIST1 argument_spec; ")"; sc = OPT scope ->
+    | "("; items = LIST1 argument_spec; ")"; sc = OPT scope_delimiter ->
        { let f x = match sc, x with
          | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x
          | Some _, Some _ -> user_err Pp.(str "scope declared twice") in
@@ -860,7 +861,7 @@ GRAMMAR EXTEND Gram
            `Id { name=name; recarg_like=recarg_like;
                  notation_scope=f notation_scope;
                  implicit_status = NotImplicit}) items }
-    | "["; items = LIST1 argument_spec; "]"; sc = OPT scope ->
+    | "["; items = LIST1 argument_spec; "]"; sc = OPT scope_delimiter ->
        { let f x = match sc, x with
          | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x
          | Some _, Some _ -> user_err Pp.(str "scope declared twice") in
@@ -868,7 +869,7 @@ GRAMMAR EXTEND Gram
            `Id { name=name; recarg_like=recarg_like;
                  notation_scope=f notation_scope;
                  implicit_status = Implicit}) items }
-    | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope ->
+    | "{"; items = LIST1 argument_spec; "}"; sc = OPT scope_delimiter ->
        { let f x = match sc, x with
          | None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x
          | Some _, Some _ -> user_err Pp.(str "scope declared twice") in
@@ -1136,11 +1137,8 @@ GRAMMAR EXTEND Gram
   positive_search_mark:
     [ [ "-" -> { false } | -> { true } ] ]
   ;
-  scope:
-    [ [ "%"; key = IDENT -> { key } ] ]
-  ;
   searchabout_query:
-    [ [ b = positive_search_mark; s = ne_string; sc = OPT scope ->
+    [ [ b = positive_search_mark; s = ne_string; sc = OPT scope_delimiter ->
             { (b, SearchString (s,sc)) }
       | b = positive_search_mark; p = constr_pattern ->
             { (b, SearchSubPattern p) }