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 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. Keep in sync with coqpp.

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 static_vernac_extend : 
  plugin:string option ->
  command:string ->
  ?classifier:(string -> vernac_classification) ->
  ?entry:Vernacexpr.vernac_expr Pcoq.Entry.t ->
  ty_ml list ->
  unit

Statically extend vernacular commands.

This is used by coqpp VERNAC EXTEND. It should not be used directly, use declare_dynamic_vernac_extend instead.

Commands added by plugins at Declare ML Module / Require time should provide plugin.

Commands added without providing plugin cannot be removed from the grammar or modified. Not passing plugin is possible for non-plugin coq-core commands and deprecated for all other callers.

Sourceval static_linking_done : unit -> unit

Used to tell the system that all future vernac extends are from plugins.

Source

val declare_dynamic_vernac_extend : 
  command:string ->
  ?entry:Vernacexpr.vernac_expr Pcoq.Entry.t ->
  depr:bool ->
  's ->
  ('r, 's) ty_sig ->
  'r ->
  Vernacexpr.extend_name

Dynamically extend vernacular commands (for instance when importing some module).

Reusing a command string will replace previous uses. The result is undefined and probably produces anomalies if the previous grammar rule is still active and was different from the new one.

The polymorphic arguments are as in TyML.

The declared grammar extension is disabled, one needs to call Egramml.extend_vernac_command_grammar in order to enable it. That call should use undoable:true to make it possible to disable the extension, e.g. by backtracking over the command which enabled it.

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

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Vernacextend`Source

VERNAC EXTEND

VERNAC ARGUMENT EXTEND

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module VernacextendSource

VERNAC EXTEND

VERNAC ARGUMENT EXTEND

Module `Vernacextend`Source