package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

Vernacular Extension data

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 Pvernac.proof_mode
  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
    (*

    Only generates opaque terms at Qed

    *)
  2. | Doesn'tGuaranteeOpacity
    (*

    May generate transparent terms even with Qed.

    *)
and solving_tac = bool

a terminator

and anon_abstracting_tac = bool

abstracting anonymously its result

and proof_block_name = string

open type of delimiters

Interpretation of extended vernac phrases.

module InProg : sig ... end
module OutProg : sig ... end
module InProof : sig ... end
module OutProof : sig ... end
type ('inprog, 'outprog, 'inproof, 'outproof) vernac_type = {
  1. inprog : 'inprog InProg.t;
  2. outprog : 'outprog InProg.t;
  3. inproof : 'inproof InProof.t;
  4. outproof : 'outproof OutProof.t;
}
type typed_vernac =
  1. | 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

val vtdefault : (unit -> unit) -> typed_vernac
val vtnoproof : (unit -> unit) -> typed_vernac
val vtcloseproof : (lemma:Declare.Proof.t -> pm:Declare.OblState.t -> Declare.OblState.t) -> typed_vernac
val vtopenproof : (unit -> Declare.Proof.t) -> typed_vernac
val vtmodifyproof : (pstate:Declare.Proof.t -> Declare.Proof.t) -> typed_vernac
val vtreadproofopt : (pstate:Declare.Proof.t option -> unit) -> typed_vernac
val vtreadproof : (pstate:Declare.Proof.t -> unit) -> typed_vernac
val vtreadprogram : (pm:Declare.OblState.t -> unit) -> typed_vernac
val vtmodifyprogram : (pm:Declare.OblState.t -> Declare.OblState.t) -> typed_vernac
val vtdeclareprogram : (pm:Declare.OblState.t -> Declare.Proof.t) -> typed_vernac
type vernac_command = ?loc:Loc.t -> atts:Attributes.vernac_flags -> unit -> typed_vernac
type plugin_args = Genarg.raw_generic_argument list
VERNAC EXTEND
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 * ('r, 's) ty_sig -> ('a -> 'r, 'a -> 's) ty_sig
type ty_ml =
  1. | TyML : bool * ('r, 's) ty_sig * 'r * 's option -> ty_ml
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
type 'a argument_rule =
  1. | 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.

    *)
  2. | 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.

    *)
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 : plugin:string -> name:string -> 'a vernac_argument -> ('a, unit, unit) Genarg.genarg_type * 'a Pcoq.Entry.t
val get_vernac_classifier : Vernacexpr.extend_name -> classifier

STM classifiers

val classify_as_query : vernac_classification

Standard constant classifiers

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