Module `Vernacextend`Source

Vernacular Extension data

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 string
| 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.

Sourcetype 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

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 : 
  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 : 
  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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.vernac/Vernacextend/index.html

Module `Vernacextend`Source

VERNAC EXTEND

VERNAC ARGUMENT EXTEND

package coq

Install

Dune Dependency

Authors

Maintainers

Sources

doc/coq-core.vernac/Vernacextend/index.html

Module VernacextendSource

VERNAC EXTEND

VERNAC ARGUMENT EXTEND

Module `Vernacextend`Source