aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/doc/parsing.md2
-rw-r--r--doc/changelog/07-commands-and-options/13096-drop-grammar-prefixes.rst6
-rw-r--r--doc/sphinx/user-extensions/syntax-extensions.rst10
-rw-r--r--doc/tools/docgram/fullGrammar1
-rw-r--r--doc/tools/docgram/orderedGrammar1
-rw-r--r--parsing/pcoq.ml109
-rw-r--r--parsing/pcoq.mli25
-rw-r--r--plugins/funind/g_indfun.mlg2
-rw-r--r--plugins/ltac/g_ltac.mlg6
-rw-r--r--plugins/ltac/g_obligations.mlg2
-rw-r--r--plugins/ltac/g_rewrite.mlg2
-rw-r--r--plugins/ltac/pltac.ml36
-rw-r--r--plugins/ltac/tacentries.ml2
-rw-r--r--plugins/ssr/ssrparser.mlg2
-rw-r--r--test-suite/output/Notations4.out8
-rw-r--r--user-contrib/Ltac2/g_ltac2.mlg14
-rw-r--r--user-contrib/Ltac2/tac2entries.ml46
-rw-r--r--vernac/egramcoq.ml8
-rw-r--r--vernac/g_vernac.mlg40
-rw-r--r--vernac/metasyntax.ml2
-rw-r--r--vernac/pvernac.ml24
-rw-r--r--vernac/pvernac.mli4
-rw-r--r--vernac/vernacextend.ml2
23 files changed, 179 insertions, 175 deletions
diff --git a/dev/doc/parsing.md b/dev/doc/parsing.md
index f8b4537e77..4982e3e94d 100644
--- a/dev/doc/parsing.md
+++ b/dev/doc/parsing.md
@@ -73,7 +73,7 @@ very specific to Coq (not so similar to Camlp5):
END
```
- Global nonterminals are declared in `pcoq.ml`, e.g. `let bignat = Entry.create "Prim.bignat"`.
+ Global nonterminals are declared in `pcoq.ml`, e.g. `let bignat = Entry.create "bignat"`.
All the `*.mlg` files include `open Pcoq` and often its modules, e.g. `open Pcoq.Prim`.
`GRAMMAR EXTEND` should be used only for large syntax additions. To add new commands
diff --git a/doc/changelog/07-commands-and-options/13096-drop-grammar-prefixes.rst b/doc/changelog/07-commands-and-options/13096-drop-grammar-prefixes.rst
new file mode 100644
index 0000000000..0ab9a58e6f
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/13096-drop-grammar-prefixes.rst
@@ -0,0 +1,6 @@
+- **Changed:**
+ Drop prefixes from grammar non-terminal names,
+ e.g. "constr:global" -> "global", "Prim.name" -> "name".
+ Visible in the output of :cmd:`Print Grammar` and :cmd:`Print Custom Grammar`.
+ (`#13096 <https://github.com/coq/coq/pull/13096>`_,
+ by Jim Fehrle).
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 6ba53b581b..5148fa84c9 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -429,10 +429,6 @@ Displaying information about notations
productions shown by `Print Grammar tactic` refer to nonterminals `tactic_then_locality`
and `tactic_then_gen` which are not shown and can't be printed.
- The prefixes `tactic:`, `prim:`, `constr:` appearing in the output are meant to identify
- what part of the grammar a nonterminal is from. If you examine nonterminal definitions
- in the source code, they are identified only by the name following the colon.
-
Most of the grammar in the documentation was updated in 8.12 to make it accurate and
readable. This was done using a new developer tool that extracts the grammar from the
source code, edits it and inserts it into the documentation files. While the
@@ -467,11 +463,11 @@ Displaying information about notations
`tactic_expr`, designated as "5", "4" and "3". Level 3 is right-associative,
which applies to the productions within it, such as the `try` construct::
- Entry tactic:tactic_expr is
+ Entry tactic_expr is
[ "5" RIGHTA
- [ tactic:binder_tactic ]
+ [ binder_tactic ]
| "4" LEFTA
- [ SELF; ";"; tactic:binder_tactic
+ [ SELF; ";"; binder_tactic
| SELF; ";"; SELF
| SELF; ";"; tactic_then_locality; tactic_then_gen; "]" ]
| "3" RIGHTA
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 2ee8e4347e..328175e65c 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1761,7 +1761,6 @@ int_or_id: [
]
language: [
-| "Ocaml" (* extraction plugin *)
| "OCaml" (* extraction plugin *)
| "Haskell" (* extraction plugin *)
| "Scheme" (* extraction plugin *)
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index aae96fc966..6ae99880b3 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -1268,7 +1268,6 @@ int_or_id: [
]
language: [
-| "Ocaml" (* extraction plugin *)
| "OCaml" (* extraction plugin *)
| "Haskell" (* extraction plugin *)
| "Scheme" (* extraction plugin *)
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
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index a1094e39a4..bbc4df7dde 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -151,7 +151,7 @@ let (wit_function_rec_definition_loc : Vernacexpr.fixpoint_expr Loc.located Gena
Genarg.create_arg "function_rec_definition_loc"
let function_rec_definition_loc =
- Pcoq.create_generic_entry Pcoq.utactic "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc)
+ Pcoq.create_generic_entry2 "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc)
}
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index d88cda177e..be0d71ad46 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -48,14 +48,14 @@ let reference_to_id qid =
CErrors.user_err ?loc:qid.CAst.loc
(str "This expression should be a simple identifier.")
-let tactic_mode = Entry.create "vernac:tactic_command"
+let tactic_mode = Entry.create "tactic_command"
let new_entry name =
let e = Entry.create name in
e
-let toplevel_selector = new_entry "vernac:toplevel_selector"
-let tacdef_body = new_entry "tactic:tacdef_body"
+let toplevel_selector = new_entry "toplevel_selector"
+let tacdef_body = new_entry "tacdef_body"
(* Registers [tactic_mode] as a parser for proof editing *)
let classic_proof_mode = Pvernac.register_proof_mode "Classic" tactic_mode
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index a6673699af..fc24475a62 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -56,7 +56,7 @@ type 'a withtac_argtype = (Tacexpr.raw_tactic_expr option, 'a) Genarg.abstract_a
let wit_withtac : Tacexpr.raw_tactic_expr option Genarg.uniform_genarg_type =
Genarg.create_arg "withtac"
-let withtac = Pcoq.create_generic_entry Pcoq.utactic "withtac" (Genarg.rawwit wit_withtac)
+let withtac = Pcoq.create_generic_entry2 "withtac" (Genarg.rawwit wit_withtac)
}
diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 09cdc997ab..8331927cda 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -219,7 +219,7 @@ type binders_argtype = local_binder_expr list
let wit_binders =
(Genarg.create_arg "binders" : binders_argtype Genarg.uniform_genarg_type)
-let binders = Pcoq.create_generic_entry Pcoq.utactic "binders" (Genarg.rawwit wit_binders)
+let binders = Pcoq.create_generic_entry2 "binders" (Genarg.rawwit wit_binders)
let () =
let raw_printer env sigma _ _ _ l = Pp.pr_non_empty_arg (Ppconstr.pr_binders env sigma) l in
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml
index 5b5ee64a56..b7b54143df 100644
--- a/plugins/ltac/pltac.ml
+++ b/plugins/ltac/pltac.ml
@@ -11,39 +11,37 @@
open Pcoq
(* Main entry for extensions *)
-let simple_tactic = Entry.create "tactic:simple_tactic"
-
-let make_gen_entry _ name = Entry.create ("tactic:" ^ name)
+let simple_tactic = Entry.create "simple_tactic"
(* Typically for tactic user extensions *)
let open_constr =
- make_gen_entry utactic "open_constr"
+ Entry.create "open_constr"
let constr_with_bindings =
- make_gen_entry utactic "constr_with_bindings"
+ Entry.create "constr_with_bindings"
let bindings =
- make_gen_entry utactic "bindings"
+ Entry.create "bindings"
let hypident = Entry.create "hypident"
-let constr_may_eval = make_gen_entry utactic "constr_may_eval"
-let constr_eval = make_gen_entry utactic "constr_eval"
+let constr_may_eval = Entry.create "constr_may_eval"
+let constr_eval = Entry.create "constr_eval"
let uconstr =
- make_gen_entry utactic "uconstr"
+ Entry.create "uconstr"
let quantified_hypothesis =
- make_gen_entry utactic "quantified_hypothesis"
-let destruction_arg = make_gen_entry utactic "destruction_arg"
-let int_or_var = make_gen_entry utactic "int_or_var"
+ Entry.create "quantified_hypothesis"
+let destruction_arg = Entry.create "destruction_arg"
+let int_or_var = Entry.create "int_or_var"
let simple_intropattern =
- make_gen_entry utactic "simple_intropattern"
-let in_clause = make_gen_entry utactic "in_clause"
+ Entry.create "simple_intropattern"
+let in_clause = Entry.create "in_clause"
let clause_dft_concl =
- make_gen_entry utactic "clause"
+ Entry.create "clause"
(* Main entries for ltac *)
-let tactic_arg = Entry.create "tactic:tactic_arg"
-let tactic_expr = make_gen_entry utactic "tactic_expr"
-let binder_tactic = make_gen_entry utactic "binder_tactic"
+let tactic_arg = Entry.create "tactic_arg"
+let tactic_expr = Entry.create "tactic_expr"
+let binder_tactic = Entry.create "binder_tactic"
-let tactic = make_gen_entry utactic "tactic"
+let tactic = Entry.create "tactic"
(* Main entry for quotations *)
let tactic_eoi = eoi_entry tactic
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index fcd60ea250..f0ca813b08 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -869,7 +869,7 @@ let argument_extend (type a b c) ~name (arg : (a, b, c) tactic_argument) =
let () = Pcoq.register_grammar wit e in
e
| Vernacextend.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 {pos=None; data=[(None, None, rules)]} in
e
in
diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg
index b32b58062a..89e0c9fcbe 100644
--- a/plugins/ssr/ssrparser.mlg
+++ b/plugins/ssr/ssrparser.mlg
@@ -403,7 +403,7 @@ END
let pr_mmod = function May -> str "?" | Must -> str "!" | Once -> mt ()
let wit_ssrmmod = add_genarg "ssrmmod" (fun env sigma -> pr_mmod)
-let ssrmmod = Pcoq.create_generic_entry Pcoq.utactic "ssrmmod" (Genarg.rawwit wit_ssrmmod);;
+let ssrmmod = Pcoq.create_generic_entry2 "ssrmmod" (Genarg.rawwit wit_ssrmmod);;
}
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index ce51acac95..a42518822f 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -1,6 +1,6 @@
[< 0 > + < 1 > * < 2 >]
: nat
-Entry constr:myconstr is
+Entry custom:myconstr is
[ "6" RIGHTA
[ ]
| "5" RIGHTA
@@ -8,7 +8,7 @@ Entry constr:myconstr is
| "4" RIGHTA
[ SELF; "*"; NEXT ]
| "3" RIGHTA
- [ "<"; constr:operconstr LEVEL "10"; ">" ] ]
+ [ "<"; operconstr LEVEL "10"; ">" ] ]
[< b > + < b > * < 2 >]
: nat
@@ -75,9 +75,9 @@ The command has indeed failed with message:
The format is not the same on the right- and left-hand sides of the special token "..".
The command has indeed failed with message:
The format is not the same on the right- and left-hand sides of the special token "..".
-Entry constr:expr is
+Entry custom:expr is
[ "201" RIGHTA
- [ "{"; constr:operconstr LEVEL "200"; "}" ] ]
+ [ "{"; operconstr LEVEL "200"; "}" ] ]
fun x : nat => [ x ]
: nat -> nat
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index d42a935104..5ae8f4ae6e 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -72,13 +72,13 @@ let test_ltac1_env =
end
let tac2expr = Tac2entries.Pltac.tac2expr
-let tac2type = Entry.create "tactic:tac2type"
-let tac2def_val = Entry.create "tactic:tac2def_val"
-let tac2def_typ = Entry.create "tactic:tac2def_typ"
-let tac2def_ext = Entry.create "tactic:tac2def_ext"
-let tac2def_syn = Entry.create "tactic:tac2def_syn"
-let tac2def_mut = Entry.create "tactic:tac2def_mut"
-let tac2mode = Entry.create "vernac:ltac2_command"
+let tac2type = Entry.create "tac2type"
+let tac2def_val = Entry.create "tac2def_val"
+let tac2def_typ = Entry.create "tac2def_typ"
+let tac2def_ext = Entry.create "tac2def_ext"
+let tac2def_syn = Entry.create "tac2def_syn"
+let tac2def_mut = Entry.create "tac2def_mut"
+let tac2mode = Entry.create "ltac2_command"
let ltac1_expr = Pltac.tactic_expr
let tac2expr_in_env = Tac2entries.Pltac.tac2expr_in_env
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 0a6e976db8..30340cd632 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -24,29 +24,29 @@ open Tac2intern
module Pltac =
struct
-let tac2expr = Pcoq.Entry.create "tactic:tac2expr"
-let tac2expr_in_env = Pcoq.Entry.create "tactic:tac2expr_in_env"
-
-let q_ident = Pcoq.Entry.create "tactic:q_ident"
-let q_bindings = Pcoq.Entry.create "tactic:q_bindings"
-let q_with_bindings = Pcoq.Entry.create "tactic:q_with_bindings"
-let q_intropattern = Pcoq.Entry.create "tactic:q_intropattern"
-let q_intropatterns = Pcoq.Entry.create "tactic:q_intropatterns"
-let q_destruction_arg = Pcoq.Entry.create "tactic:q_destruction_arg"
-let q_induction_clause = Pcoq.Entry.create "tactic:q_induction_clause"
-let q_conversion = Pcoq.Entry.create "tactic:q_conversion"
-let q_rewriting = Pcoq.Entry.create "tactic:q_rewriting"
-let q_clause = Pcoq.Entry.create "tactic:q_clause"
-let q_dispatch = Pcoq.Entry.create "tactic:q_dispatch"
-let q_occurrences = Pcoq.Entry.create "tactic:q_occurrences"
-let q_reference = Pcoq.Entry.create "tactic:q_reference"
-let q_strategy_flag = Pcoq.Entry.create "tactic:q_strategy_flag"
-let q_constr_matching = Pcoq.Entry.create "tactic:q_constr_matching"
-let q_goal_matching = Pcoq.Entry.create "tactic:q_goal_matching"
-let q_hintdb = Pcoq.Entry.create "tactic:q_hintdb"
-let q_move_location = Pcoq.Entry.create "tactic:q_move_location"
-let q_pose = Pcoq.Entry.create "tactic:q_pose"
-let q_assert = Pcoq.Entry.create "tactic:q_assert"
+let tac2expr = Pcoq.Entry.create "tac2expr"
+let tac2expr_in_env = Pcoq.Entry.create "tac2expr_in_env"
+
+let q_ident = Pcoq.Entry.create "q_ident"
+let q_bindings = Pcoq.Entry.create "q_bindings"
+let q_with_bindings = Pcoq.Entry.create "q_with_bindings"
+let q_intropattern = Pcoq.Entry.create "q_intropattern"
+let q_intropatterns = Pcoq.Entry.create "q_intropatterns"
+let q_destruction_arg = Pcoq.Entry.create "q_destruction_arg"
+let q_induction_clause = Pcoq.Entry.create "q_induction_clause"
+let q_conversion = Pcoq.Entry.create "q_conversion"
+let q_rewriting = Pcoq.Entry.create "q_rewriting"
+let q_clause = Pcoq.Entry.create "q_clause"
+let q_dispatch = Pcoq.Entry.create "q_dispatch"
+let q_occurrences = Pcoq.Entry.create "q_occurrences"
+let q_reference = Pcoq.Entry.create "q_reference"
+let q_strategy_flag = Pcoq.Entry.create "q_strategy_flag"
+let q_constr_matching = Pcoq.Entry.create "q_constr_matching"
+let q_goal_matching = Pcoq.Entry.create "q_goal_matching"
+let q_hintdb = Pcoq.Entry.create "q_hintdb"
+let q_move_location = Pcoq.Entry.create "q_move_location"
+let q_pose = Pcoq.Entry.create "q_pose"
+let q_assert = Pcoq.Entry.create "q_assert"
end
(** Tactic definition *)
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:43:24 +0000