Module `Vernacextend`

Vernacular Extension data

type vernac_keep_as = | VtKeepAxiom | VtKeepDefined | VtKeepOpaque
type vernac_qed_type = | VtKeep of vernac_keep_as | VtDrop
type vernac_when = | VtNow | VtLater
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 string | VtMeta
and vernac_start = opacity_guarantee * Names.Id.t list
and vernac_sideff_type = Names.Id.t list * vernac_when
and opacity_guarantee = | GuaranteesOpacity Only generates opaque terms at Qed | Doesn'tGuaranteeOpacity May generate transparent terms even with Qed.
and solving_tac = bool: a terminator

type typed_vernac = | VtDefault of unit -> unit | VtNoProof of unit -> unit | VtCloseProof of lemma:Declare.Proof.t -> pm:Declare.OblState.t -> Declare.OblState.t | VtOpenProof of unit -> Declare.Proof.t | VtModifyProof of pstate:Declare.Proof.t -> Declare.Proof.t | VtReadProofOpt of pstate:Declare.Proof.t option -> unit | VtReadProof of pstate:Declare.Proof.t -> unit | VtReadProgram of pm:Declare.OblState.t -> unit | VtModifyProgram of pm:Declare.OblState.t -> Declare.OblState.t | VtDeclareProgram of pm:Declare.OblState.t -> Declare.Proof.t | VtOpenProofProgram of pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t
type vernac_command = atts:Attributes.vernac_flags -> typed_vernac
type plugin_args = Genarg.raw_generic_argument list

type classifier = Genarg.raw_generic_argument list -> vernac_classification
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
type ty_ml = | TyML : bool * ('r, 's) ty_sig * 'r * 's option -> ty_ml

val vernac_extend : command:string -> ?⁠classifier:(string -> vernac_classification) -> ?⁠entry:Vernacexpr.vernac_expr Pcoq.Entry.t -> ty_ml list -> unit: Wrapper to dynamically extend vernacular commands.

type 'a argument_rule = | Arg_alias of 'a Pcoq.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 Pcoq.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 : name:string -> 'a vernac_argument -> ('a, unit, unit) Genarg.genarg_type * 'a Pcoq.Entry.t
val get_vernac_classifier : Vernacexpr.extend_name -> classifier: STM classifiers

val classify_as_query : vernac_classification: Standard constant classifiers

`\|` `GuaranteesOpacity`	Only generates opaque terms at `Qed`
`\|` `Doesn'tGuaranteeOpacity`	May generate transparent terms even with `Qed`.

`\|` `Arg_alias of 'a Pcoq.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 Pcoq.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.