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

and anon_abstracting_tac = bool

abstracting anonymously its result

and proof_block_name = string

open type of delimiters

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
val type_vernac : Vernacexpr.extend_name -> plugin_args -> vernac_command
VERNAC EXTEND
type classifier = Genarg.raw_generic_argument list -> vernac_classification
type (_, _) ty_sig =
| TyNil : (vernac_commandvernac_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 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

val classify_as_sideeff : vernac_classification
val classify_as_proofstep : vernac_classification