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. parallel : [ `No | `Yes of solving_tac * anon_abstracting_tac ];
    2. 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:Lemmas.t -> unit
  4. | VtOpenProof of unit -> Lemmas.t
  5. | VtModifyProof of pstate:Proof_global.t -> Proof_global.t
  6. | VtReadProofOpt of pstate:Proof_global.t option -> unit
  7. | VtReadProof of pstate:Proof_global.t -> unit
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 Extend.production_rule 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct