package rocq-runtime
Install
Dune Dependency
Authors
Maintainers
Sources
md5=8d522602d23e7a665631826dab9aa92b
sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be
doc/rocq-runtime.vernac/Vernacextend/index.html
Module VernacextendSource
Vernacular Extension data
type vernac_classification = | VtStartProof of vernac_start| VtSideff of vernac_sideff_type| VtQed of vernac_qed_type| VtProofStep of {proof_block_detection : proof_block_name option;
}| VtQuery| VtProofMode of Pvernac.proof_mode| VtMeta
a terminator
abstracting anonymously its result
open type of delimiters
type vernac_command =
?loc:Loc.t ->
atts:Attributes.vernac_flags ->
unit ->
Vernactypes.typed_vernacVERNAC EXTEND
type (_, _) ty_sig = | TyNil : (vernac_command, vernac_classification) ty_sig| TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig| TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig
val static_vernac_extend :
plugin:string option ->
command:string ->
?classifier:(string -> vernac_classification) ->
?entry:Vernacexpr.vernac_expr Procq.Entry.t ->
ty_ml list ->
unitStatically extend vernacular commands.
This is used by coqpp VERNAC EXTEND. It should not be used directly, use declare_dynamic_vernac_extend instead.
Commands added by plugins at Declare ML Module / Require time should provide plugin.
Commands added without providing plugin cannot be removed from the grammar or modified. Not passing plugin is possible for non-plugin rocq-runtime commands and deprecated for all other callers.
Used to tell the system that all future vernac extends are from plugins.
val declare_dynamic_vernac_extend :
command:Vernacexpr.extend_name ->
?entry:Vernacexpr.vernac_expr Procq.Entry.t ->
depr:bool ->
's ->
('r, 's) ty_sig ->
'r ->
Vernacexpr.extend_nameDynamically extend vernacular commands (for instance when importing some module).
Reusing a command string will replace previous uses. The result is undefined and probably produces anomalies if the previous grammar rule is still active and was different from the new one.
The polymorphic arguments are as in TyML.
The declared grammar extension is disabled, one needs to call Egramml.extend_vernac_command_grammar in order to enable it. That call should use undoable:true to make it possible to disable the extension, e.g. by backtracking over the command which enabled it.
VERNAC ARGUMENT EXTEND
type 'a argument_rule = | Arg_alias of 'a Procq.Entry.t(*This is used because CAMLP5 parser can be dumb about rule factorization, which sometimes requires two entries to be the same.
*)| Arg_rules of 'a Procq.Production.t list(*There is a discrepancy here as we use directly extension rules and thus entries instead of ty_user_symbol and thus arguments as roots.
*)
type 'a vernac_argument = {arg_printer : Environ.env -> Evd.evar_map -> 'a -> Pp.t;arg_parsing : 'a argument_rule;
}val vernac_argument_extend :
plugin:string ->
name:string ->
'a vernac_argument ->
'a Genarg.vernac_genarg_type * 'a Procq.Entry.tSTM classifiers
Standard constant classifiers