Module Vernacextend

Vernacular Extension data

type vernac_keep_as =
| VtKeepAxiom
| VtKeepDefined
| VtKeepOpaque
type vernac_qed_type =
| VtKeep of vernac_keep_as
| VtDrop
type vernac_type =
| VtStartProof of vernac_start
| VtSideff of vernac_sideff_type
| VtQed of vernac_qed_type
| VtProofStep of {
parallel : [ `Yes of solving_tac * anon_abstracting_tac | `No ];
proof_block_detection : proof_block_name option;
}
| VtQuery
| VtProofMode of string
| VtMeta
| VtUnknown
and vernac_start = opacity_guarantee * Names.Id.t list
and vernac_sideff_type = Names.Id.t list
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

and anon_abstracting_tac = bool

abstracting anonymously its result

and proof_block_name = string

open type of delimiters

type vernac_when =
| VtNow
| VtLater
type vernac_classification = vernac_type * vernac_when
type 'a vernac_command = 'a -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
type plugin_args = Genarg.raw_generic_argument list
val call : Vernacexpr.extend_name -> plugin_args -> atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.t
VERNAC EXTEND
type classifier = Genarg.raw_generic_argument list -> vernac_classification
type (_, _) ty_sig =
| TyNil : (atts:Attributes.vernac_flags -> st:Vernacstate.t -> Vernacstate.tvernac_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.

VERNAC ARGUMENT EXTEND
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 Extend.production_rule 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

val classify_as_sideeff : vernac_classification
val classify_as_proofstep : vernac_classification