Vernacextend (u.dc2732db2fd5639a0cf8e3e92bbaa8d7.coq-core.8.17.1.doc.coq-core.vernac.Vernacextend)

Sourcetype vernac_keep_as =

| VtKeepAxiom
| VtKeepDefined
| VtKeepOpaque

Sourcetype vernac_qed_type =

| VtKeep of vernac_keep_as
| VtDrop

Sourcetype vernac_when =

| VtNow
| VtLater

Sourcetype vernac_classification =

| VtStartProof of vernac_start
| VtSideff of vernac_sideff_type
| VtQed of vernac_qed_type
| VtProofStep of {
1. proof_block_detection : proof_block_name option;
}
| VtQuery
| VtProofMode of Pvernac.proof_mode
| VtMeta

Sourceand vernac_start = opacity_guarantee * Names.Id.t list

Sourceand vernac_sideff_type = Names.Id.t list * vernac_when

Sourceand opacity_guarantee =

| GuaranteesOpacity
(*
Only generates opaque terms at Qed
*)
| Doesn'tGuaranteeOpacity
(*
May generate transparent terms even with Qed.
*)

Sourceand solving_tac = bool

a terminator

Sourceand anon_abstracting_tac = bool

abstracting anonymously its result

Sourceand proof_block_name = string

open type of delimiters

Interpretation of extended vernac phrases.

Sourcemodule InProg : sig ... end

Sourcemodule OutProg : sig ... end

Sourcemodule InProof : sig ... end

Sourcemodule OutProof : sig ... end

Sourcetype ('inprog, 'outprog, 'inproof, 'outproof) vernac_type = {

inprog : 'inprog InProg.t;
outprog : 'outprog InProg.t;
inproof : 'inproof InProof.t;
outproof : 'outproof OutProof.t;

}

Sourcetype typed_vernac =

| TypedVernac : {
1. inprog : 'inprog InProg.t;
2. outprog : 'outprog OutProg.t;
3. inproof : 'inproof InProof.t;
4. outproof : 'outproof OutProof.t;
5. run : pm:'inprog -> proof:'inproof -> 'outprog * 'outproof;
} -> typed_vernac

Some convenient typed_vernac constructors

Sourceval vtdefault : (unit -> unit) -> typed_vernac

Sourceval vtnoproof : (unit -> unit) -> typed_vernac

Source

val vtcloseproof : 
  (lemma:Declare.Proof.t -> pm:Declare.OblState.t -> Declare.OblState.t) ->
  typed_vernac

Sourceval vtopenproof : (unit -> Declare.Proof.t) -> typed_vernac

Sourceval vtmodifyproof : (pstate:Declare.Proof.t -> Declare.Proof.t) -> typed_vernac

Sourceval vtreadproofopt : (pstate:Declare.Proof.t option -> unit) -> typed_vernac

Sourceval vtreadproof : (pstate:Declare.Proof.t -> unit) -> typed_vernac

Sourceval vtreadprogram : (pm:Declare.OblState.t -> unit) -> typed_vernac

Source

val vtmodifyprogram : 
  (pm:Declare.OblState.t -> Declare.OblState.t) ->
  typed_vernac

Source

val vtdeclareprogram : 
  (pm:Declare.OblState.t -> Declare.Proof.t) ->
  typed_vernac

Source

val vtopenproofprogram : 
  (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t) ->
  typed_vernac

Source

type vernac_command =
  ?loc:Loc.t ->
  atts:Attributes.vernac_flags ->
  unit ->
  typed_vernac

Sourcetype plugin_args = Genarg.raw_generic_argument list

Sourceval type_vernac : Vernacexpr.extend_name -> plugin_args -> vernac_command

VERNAC EXTEND

Sourcetype classifier = Genarg.raw_generic_argument list -> vernac_classification

Sourcetype (_, _) 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

Sourcetype ty_ml =

| TyML : bool * ('r, 's) ty_sig * 'r * 's option -> ty_ml

Source

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

Sourcetype '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.
*)

Sourcetype 'a vernac_argument = {

arg_printer : Environ.env -> Evd.evar_map -> 'a -> Pp.t;
arg_parsing : 'a argument_rule;

}

Source

val vernac_argument_extend : 
  plugin:string ->
  name:string ->
  'a vernac_argument ->
  ('a, unit, unit) Genarg.genarg_type * 'a Pcoq.Entry.t

Sourceval get_vernac_classifier : Vernacexpr.extend_name -> classifier

STM classifiers

Sourceval classify_as_query : vernac_classification

Standard constant classifiers

Sourceval classify_as_sideeff : vernac_classification

Sourceval classify_as_proofstep : vernac_classification