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

Reviewed-by: herbelin
Ack-by: Zimmi48

6 files changed, 41 insertions, 39 deletions

diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index cbd83e88b6..b134f7b82b 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -268,16 +268,16 @@ let custom_entry_locality = Summary.ref ~name:"LOCAL-CUSTOM-ENTRY" String.Set.em
 let create_custom_entry ~local s =
   if List.mem s ["constr";"pattern";"ident";"global";"binder";"bigint"] then
     user_err Pp.(quote (str s) ++ str " is a reserved entry name.");
-  let sc = "constr:"^s in
-  let sp = "pattern:"^s in
+  let sc = "custom:"^s in
+  let sp = "custom_pattern:"^s in
   let _ = extend_entry_command constr_custom_entry sc in
   let _ = extend_entry_command pattern_custom_entry sp in
   let () = if local then custom_entry_locality := String.Set.add s !custom_entry_locality in
   ()
 
 let find_custom_entry s =
-  let sc = "constr:"^s in
-  let sp = "pattern:"^s in
+  let sc = "custom:"^s in
+  let sp = "custom_pattern:"^s in
   try (find_custom_entry constr_custom_entry sc, find_custom_entry pattern_custom_entry sp)
   with Not_found -> user_err Pp.(str "Undeclared custom entry: " ++ str s ++ str ".")
 
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 5b039e76f3..831aeff6a0 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -33,26 +33,26 @@ open Attributes
 (* Rem: do not join the different GEXTEND into one, it breaks native *)
 (* compilation on PowerPC and Sun architectures *)
 
-let query_command = Entry.create "vernac:query_command"
-
-let search_query = Entry.create "vernac:search_query"
-let search_queries = Entry.create "vernac:search_queries"
-
-let subprf = Entry.create "vernac:subprf"
-
-let quoted_attributes = Entry.create "vernac:quoted_attributes"
-let class_rawexpr = Entry.create "vernac:class_rawexpr"
-let thm_token = Entry.create "vernac:thm_token"
-let def_token = Entry.create "vernac:def_token"
-let assumption_token = Entry.create "vernac:assumption_token"
-let def_body = Entry.create "vernac:def_body"
-let decl_notations = Entry.create "vernac:decl_notations"
-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 syntax_modifiers = Entry.create "vernac:syntax_modifiers"
-let only_parsing = Entry.create "vernac:only_parsing"
+let query_command = Entry.create "query_command"
+
+let search_query = Entry.create "search_query"
+let search_queries = Entry.create "search_queries"
+
+let subprf = Entry.create "subprf"
+
+let quoted_attributes = Entry.create "quoted_attributes"
+let class_rawexpr = Entry.create "class_rawexpr"
+let thm_token = Entry.create "thm_token"
+let def_token = Entry.create "def_token"
+let assumption_token = Entry.create "assumption_token"
+let def_body = Entry.create "def_body"
+let decl_notations = Entry.create "decl_notations"
+let record_field = Entry.create "record_field"
+let of_type_with_opt_coercion = Entry.create "of_type_with_opt_coercion"
+let section_subset_expr = Entry.create "section_subset_expr"
+let scope_delimiter = Entry.create "scope_delimiter"
+let syntax_modifiers = Entry.create "syntax_modifiers"
+let only_parsing = Entry.create "only_parsing"
 
 let make_bullet s =
   let open Proof_bullet in
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index ab1ce44081..898a262266 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -85,7 +85,7 @@ let pr_grammar = function
       pr_entry Pvernac.Vernac_.gallina_ext
   | name -> pr_registered_grammar name
 
-let pr_custom_grammar name = pr_registered_grammar ("constr:"^name)
+let pr_custom_grammar name = pr_registered_grammar ("custom:"^name)
 
 (**********************************************************************)
 (* Parse a format (every terminal starting with a letter or a single
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index f4cb1adfe8..c9f68eed57 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -10,7 +10,9 @@
 
 open Pcoq
 
-let uvernac = create_universe "vernac"
+[@@@ocaml.warning "-3"]
+let uvernac = create_universe "vernac" [@@deprecated "Deprecated in 8.13"]
+[@@@ocaml.warning "+3"]
 
 type proof_mode = string
 
@@ -35,20 +37,18 @@ let command_entry_ref = ref None
 
 module Vernac_ =
   struct
-    let gec_vernac s = Entry.create ("vernac:" ^ s)
-
     (* The different kinds of vernacular commands *)
-    let gallina = gec_vernac "gallina"
-    let gallina_ext = gec_vernac "gallina_ext"
-    let command = gec_vernac "command"
-    let syntax = gec_vernac "syntax_command"
-    let vernac_control = gec_vernac "Vernac.vernac_control"
-    let rec_definition = gec_vernac "Vernac.rec_definition"
-    let red_expr = new_entry utactic "red_expr"
-    let hint_info = gec_vernac "hint_info"
+    let gallina = Entry.create "gallina"
+    let gallina_ext = Entry.create "gallina_ext"
+    let command = Entry.create "command"
+    let syntax = Entry.create "syntax_command"
+    let vernac_control = Entry.create "Vernac.vernac_control"
+    let rec_definition = Entry.create "Vernac.rec_definition"
+    let red_expr = Entry.create "red_expr"
+    let hint_info = Entry.create "hint_info"
     (* Main vernac entry *)
     let main_entry = Entry.create "vernac"
-    let noedit_mode = gec_vernac "noedit_command"
+    let noedit_mode = Entry.create "noedit_command"
 
     let () =
       let act_vernac v loc = Some v in
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index 1718024edd..8ab4af7d48 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -12,7 +12,9 @@ open Pcoq
 open Genredexpr
 open Vernacexpr
 
-val uvernac : gram_universe
+[@@@ocaml.warning "-3"]
+val uvernac : gram_universe [@@deprecated "Deprecated in 8.13"]
+[@@@ocaml.warning "+3"]
 
 type proof_mode
 
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 496b1a43d1..eacb7fe6cb 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -247,7 +247,7 @@ let vernac_argument_extend ~name arg =
     let () = Pcoq.register_grammar wit e in
     e
   | Arg_rules rules ->
-    let e = Pcoq.create_generic_entry Pcoq.utactic name (Genarg.rawwit wit) in
+    let e = Pcoq.create_generic_entry2 name (Genarg.rawwit wit) in
     let () = Pcoq.grammar_extend e {Pcoq.pos=None; data=[(None, None, rules)]} in
     e
   in