Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" -> "constr"

Reviewed-by: herbelin
Ack-by: Zimmi48

2 files changed, 69 insertions, 65 deletions

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
index 0d74ad928c..723f08413e 100644
--- a/parsing/pcoq.ml
+++ b/parsing/pcoq.ml
@@ -202,6 +202,7 @@ let parse_string f ?loc x =
   let strm = Stream.of_string x in
   Entry.parse f (Parsable.make ?loc strm)
 
+(* universes not used by Coq build but still used by some plugins *)
 type gram_universe = string
 
 let utables : (string, unit) Hashtbl.t =
@@ -211,21 +212,18 @@ let create_universe u =
   let () = Hashtbl.add utables u () in
   u
 
-let uprim   = create_universe "prim"
-let uconstr = create_universe "constr"
-let utactic = create_universe "tactic"
+let uprim   = create_universe "prim" [@@deprecated "Deprecated in 8.13"]
+let uconstr = create_universe "constr" [@@deprecated "Deprecated in 8.13"]
+let utactic = create_universe "tactic" [@@deprecated "Deprecated in 8.13"]
 
 let get_univ u =
   if Hashtbl.mem utables u then u
   else raise Not_found
 
-let new_entry u s =
-  let ename = u ^ ":" ^ s in
-  let e = Entry.make ename in
+let new_entry _ s =
+  let e = Entry.make s in
   e
 
-let make_gen_entry u s = new_entry u s
-
 module GrammarObj =
 struct
   type ('r, _, _) obj = 'r Entry.t
@@ -251,52 +249,54 @@ let genarg_grammar x =
   check_compatibility x;
   Grammar.obj x
 
-let create_generic_entry (type a) u s (etyp : a raw_abstract_argument_type) : a Entry.t =
-  let e = new_entry u s in
+let create_generic_entry2 (type a) s (etyp : a raw_abstract_argument_type) : a Entry.t =
+  let e = Entry.create s in
   let Rawwit t = etyp in
   let () = Grammar.register0 t e in
   e
 
+let create_generic_entry (type a) _ s (etyp : a raw_abstract_argument_type) : a Entry.t =
+  create_generic_entry2 s etyp
+
 (* Initial grammar entries *)
 
 module Prim =
   struct
-    let gec_gen n = make_gen_entry uprim n
 
     (* Entries that can be referred via the string -> Entry.t table *)
     (* Typically for tactic or vernac extensions *)
-    let preident = gec_gen "preident"
-    let ident = gec_gen "ident"
-    let natural = gec_gen "natural"
-    let integer = gec_gen "integer"
-    let bignat = Entry.create "Prim.bignat"
-    let bigint = Entry.create "Prim.bigint"
-    let string = gec_gen "string"
-    let lstring = Entry.create "Prim.lstring"
-    let reference = make_gen_entry uprim "reference"
+    let preident = Entry.create "preident"
+    let ident = Entry.create "ident"
+    let natural = Entry.create "natural"
+    let integer = Entry.create "integer"
+    let bignat = Entry.create "bignat"
+    let bigint = Entry.create "bigint"
+    let string = Entry.create "string"
+    let lstring = Entry.create "lstring"
+    let reference = Entry.create "reference"
     let by_notation = Entry.create "by_notation"
     let smart_global = Entry.create "smart_global"
-    let strategy_level = gec_gen "strategy_level"
+    let strategy_level = Entry.create "strategy_level"
 
     (* parsed like ident but interpreted as a term *)
-    let var = gec_gen "var"
+    let var = Entry.create "var"
 
-    let name = Entry.create "Prim.name"
-    let identref = Entry.create "Prim.identref"
-    let univ_decl = Entry.create "Prim.univ_decl"
-    let ident_decl = Entry.create "Prim.ident_decl"
+    let name = Entry.create "name"
+    let identref = Entry.create "identref"
+    let univ_decl = Entry.create "univ_decl"
+    let ident_decl = Entry.create "ident_decl"
     let pattern_ident = Entry.create "pattern_ident"
     let pattern_identref = Entry.create "pattern_identref"
 
     (* A synonym of ident - maybe ident will be located one day *)
-    let base_ident = Entry.create "Prim.base_ident"
+    let base_ident = Entry.create "base_ident"
 
-    let qualid = Entry.create "Prim.qualid"
-    let fullyqualid = Entry.create "Prim.fullyqualid"
-    let dirpath = Entry.create "Prim.dirpath"
+    let qualid = Entry.create "qualid"
+    let fullyqualid = Entry.create "fullyqualid"
+    let dirpath = Entry.create "dirpath"
 
-    let ne_string = Entry.create "Prim.ne_string"
-    let ne_lstring = Entry.create "Prim.ne_lstring"
+    let ne_string = Entry.create "ne_string"
+    let ne_lstring = Entry.create "ne_lstring"
 
     let bar_cbrace = Entry.create "'|}'"
 
@@ -304,32 +304,31 @@ module Prim =
 
 module Constr =
   struct
-    let gec_constr = make_gen_entry uconstr
 
     (* Entries that can be referred via the string -> Entry.t table *)
-    let constr = gec_constr "constr"
-    let operconstr = gec_constr "operconstr"
+    let constr = Entry.create "constr"
+    let operconstr = Entry.create "operconstr"
     let constr_eoi = eoi_entry constr
-    let lconstr = gec_constr "lconstr"
-    let binder_constr = gec_constr "binder_constr"
-    let ident = make_gen_entry uconstr "ident"
-    let global = make_gen_entry uconstr "global"
-    let universe_name = make_gen_entry uconstr "universe_name"
-    let universe_level = make_gen_entry uconstr "universe_level"
-    let sort = make_gen_entry uconstr "sort"
-    let sort_family = make_gen_entry uconstr "sort_family"
-    let pattern = Entry.create "constr:pattern"
-    let constr_pattern = gec_constr "constr_pattern"
-    let lconstr_pattern = gec_constr "lconstr_pattern"
-    let closed_binder = Entry.create "constr:closed_binder"
-    let binder = Entry.create "constr:binder"
-    let binders = Entry.create "constr:binders"
-    let open_binders = Entry.create "constr:open_binders"
-    let binders_fixannot = Entry.create "constr:binders_fixannot"
-    let typeclass_constraint = Entry.create "constr:typeclass_constraint"
-    let record_declaration = Entry.create "constr:record_declaration"
-    let appl_arg = Entry.create "constr:appl_arg"
-    let type_cstr = Entry.create "constr:type_cstr"
+    let lconstr = Entry.create "lconstr"
+    let binder_constr = Entry.create "binder_constr"
+    let ident = Entry.create "ident"
+    let global = Entry.create "global"
+    let universe_name = Entry.create "universe_name"
+    let universe_level = Entry.create "universe_level"
+    let sort = Entry.create "sort"
+    let sort_family = Entry.create "sort_family"
+    let pattern = Entry.create "pattern"
+    let constr_pattern = Entry.create "constr_pattern"
+    let lconstr_pattern = Entry.create "lconstr_pattern"
+    let closed_binder = Entry.create "closed_binder"
+    let binder = Entry.create "binder"
+    let binders = Entry.create "binders"
+    let open_binders = Entry.create "open_binders"
+    let binders_fixannot = Entry.create "binders_fixannot"
+    let typeclass_constraint = Entry.create "typeclass_constraint"
+    let record_declaration = Entry.create "record_declaration"
+    let appl_arg = Entry.create "appl_arg"
+    let type_cstr = Entry.create "type_cstr"
   end
 
 module Module =
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index bd64d21518..ae9a7423c2 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -123,24 +123,29 @@ val parse_string : 'a Entry.t -> ?loc:Loc.t -> string -> 'a
 val eoi_entry : 'a Entry.t -> 'a Entry.t
 val map_entry : ('a -> 'b) -> 'a Entry.t -> 'b Entry.t
 
-type gram_universe
+type gram_universe [@@deprecated "Deprecated in 8.13"]
+[@@@ocaml.warning "-3"]
+val get_univ : string -> gram_universe [@@deprecated "Deprecated in 8.13"]
+val create_universe : string -> gram_universe [@@deprecated "Deprecated in 8.13"]
 
-val get_univ : string -> gram_universe
-val create_universe : string -> gram_universe
+val new_entry : gram_universe -> string -> 'a Entry.t [@@deprecated "Deprecated in 8.13"]
 
-val new_entry : gram_universe -> string -> 'a Entry.t
+val uprim : gram_universe [@@deprecated "Deprecated in 8.13"]
+val uconstr : gram_universe [@@deprecated "Deprecated in 8.13"]
+val utactic : gram_universe [@@deprecated "Deprecated in 8.13"]
 
-val uprim : gram_universe
-val uconstr : gram_universe
-val utactic : gram_universe
+val create_generic_entry : gram_universe -> string ->
+  ('a, rlevel) abstract_argument_type -> 'a Entry.t
+  [@@deprecated "Deprecated in 8.13.  Use create_generic_entry2 instead."]
+[@@@ocaml.warning "+3"]
+
+val create_generic_entry2 : string ->
+  ('a, rlevel) abstract_argument_type -> 'a Entry.t
 
 
 val register_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Entry.t -> unit
 val genarg_grammar : ('raw, 'glb, 'top) genarg_type -> 'raw Entry.t
 
-val create_generic_entry : gram_universe -> string ->
-  ('a, rlevel) abstract_argument_type -> 'a Entry.t
-
 module Prim :
   sig
     open Names