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 stack:Vernacstate.LemmaStack.t option -> 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
= ?loc:Loc.t -> atts:Attributes.vernac_flags -> unit -> 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_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.
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