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 Pvernac.proof_mode
| 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

Interpretation of extended vernac phrases.

module InProg : sig ... end
module OutProg : sig ... end
module InProof : sig ... end
module OutProof : sig ... end
type ('inprog, 'outprog, 'inproof, 'outproof) vernac_type = {
inprog : 'inprog InProg.t;
outprog : 'outprog InProg.t;
inproof : 'inproof InProof.t;
outproof : 'outproof OutProof.t;
}
type typed_vernac =
| TypedVernac : {
inprog : 'inprog InProg.t;
outprog : 'outprog OutProg.t;
inproof : 'inproof InProof.t;
outproof : 'outproof OutProof.t;
run : pm:'inprog -> proof:'inproof -> 'outprog * 'outproof;
} -> typed_vernac

Some convenient typed_vernac constructors

val vtdefault : (unit -> unit) -> typed_vernac
val vtnoproof : (unit -> unit) -> typed_vernac
val vtcloseproof : (lemma:Declare.Proof.t -> pm:Declare.OblState.t -> Declare.OblState.t) -> typed_vernac
val vtopenproof : (unit -> Declare.Proof.t) -> typed_vernac
val vtmodifyproof : (pstate:Declare.Proof.t -> Declare.Proof.t) -> typed_vernac
val vtreadproofopt : (pstate:Declare.Proof.t option -> unit) -> typed_vernac
val vtreadproof : (pstate:Declare.Proof.t -> unit) -> typed_vernac
val vtreadprogram : (pm:Declare.OblState.t -> unit) -> typed_vernac
val vtmodifyprogram : (pm:Declare.OblState.t -> Declare.OblState.t) -> typed_vernac
val vtdeclareprogram : (pm:Declare.OblState.t -> Declare.Proof.t) -> typed_vernac
type vernac_command = ?loc:Loc.t -> atts:Attributes.vernac_flags -> unit -> typed_vernac
type plugin_args = Genarg.raw_generic_argument list
VERNAC 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
type ty_ml =
| TyML : bool * ('r, 's) ty_sig * 'r * 's option -> ty_ml
val vernac_extend : ?plugin:string -> 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 : plugin:string -> 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