package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
type vernac_keep_as =
  1. | VtKeepAxiom
  2. | VtKeepDefined
  3. | VtKeepOpaque
type vernac_qed_type =
  1. | VtKeep of vernac_keep_as
  2. | VtDrop
type vernac_when =
  1. | VtNow
  2. | VtLater
type vernac_classification =
  1. | VtStartProof of vernac_start
  2. | VtSideff of vernac_sideff_type
  3. | VtQed of vernac_qed_type
  4. | VtProofStep of {
    1. proof_block_detection : proof_block_name option;
    }
  5. | VtQuery
  6. | VtProofMode of string
  7. | VtMeta
and vernac_start = opacity_guarantee * Names.Id.t list
and vernac_sideff_type = Names.Id.t list * vernac_when
and opacity_guarantee =
  1. | GuaranteesOpacity
  2. | Doesn'tGuaranteeOpacity
and solving_tac = bool
and anon_abstracting_tac = bool
and proof_block_name = string
type typed_vernac =
  1. | VtDefault of unit -> unit
  2. | VtNoProof of unit -> unit
  3. | VtCloseProof of lemma:Declare.Proof.t -> pm:Declare.OblState.t -> Declare.OblState.t
  4. | VtOpenProof of unit -> Declare.Proof.t
  5. | VtModifyProof of pstate:Declare.Proof.t -> Declare.Proof.t
  6. | VtReadProofOpt of pstate:Declare.Proof.t option -> unit
  7. | VtReadProof of pstate:Declare.Proof.t -> unit
  8. | VtReadProgram of pm:Declare.OblState.t -> unit
  9. | VtModifyProgram of pm:Declare.OblState.t -> Declare.OblState.t
  10. | VtDeclareProgram of pm:Declare.OblState.t -> Declare.Proof.t
  11. | VtOpenProofProgram of pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t
type vernac_command = atts:Attributes.vernac_flags -> typed_vernac
type plugin_args = Genarg.raw_generic_argument list
type (!_, !_) ty_sig =
  1. | TyNil : (vernac_command, vernac_classification) ty_sig
  2. | TyTerminal : string * ('r, 's) ty_sig -> ('r, 's) ty_sig
  3. | TyNonTerminal : ('a, 'b, 'c) Extend.ty_user_symbol * ('r0, 's0) ty_sig -> ('a -> 'r0, 'a -> 's0) ty_sig
type ty_ml =
  1. | 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
type !'a argument_rule =
  1. | Arg_alias of 'a Pcoq.Entry.t
  2. | Arg_rules of 'a Pcoq.Production.t list
type !'a vernac_argument = {
  1. arg_printer : Environ.env -> Evd.evar_map -> 'a -> Pp.t;
  2. 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
val classify_as_query : vernac_classification
val classify_as_sideeff : vernac_classification
val classify_as_proofstep : vernac_classification