package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.17.1.tar.gz
sha512=9a35311acec2a806730b94ac7dceabc88837f235c52a14c026827d9b89433bd7fa9555a9fc6829aa49edfedb24c8bbaf1411ebf463b74a50aeb17cba47745b6b

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

Module VernacextendSource

Vernacular Extension data

Sourcetype vernac_keep_as =
  1. | VtKeepAxiom
  2. | VtKeepDefined
  3. | VtKeepOpaque
Sourcetype vernac_qed_type =
  1. | VtKeep of vernac_keep_as
  2. | VtDrop
Sourcetype vernac_when =
  1. | VtNow
  2. | VtLater
Sourcetype 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
Sourceand vernac_start = opacity_guarantee * Names.Id.t list
Sourceand vernac_sideff_type = Names.Id.t list * vernac_when
Sourceand opacity_guarantee =
  1. | GuaranteesOpacity
    (*

    Only generates opaque terms at Qed

    *)
  2. | 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 = {
  1. inprog : 'inprog InProg.t;
  2. outprog : 'outprog InProg.t;
  3. inproof : 'inproof InProof.t;
  4. outproof : 'outproof OutProof.t;
}
Sourcetype 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

Sourceval vtdefault : (unit -> unit) -> typed_vernac
Sourceval vtnoproof : (unit -> unit) -> 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
Sourceval vtdeclareprogram : (pm:Declare.OblState.t -> Declare.Proof.t) -> typed_vernac
Sourcetype vernac_command = ?loc:Loc.t -> atts:Attributes.vernac_flags -> unit -> typed_vernac
Sourcetype plugin_args = Genarg.raw_generic_argument list
VERNAC EXTEND
Sourcetype (_, _) 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
Sourcetype ty_ml =
  1. | TyML : bool * ('r, 's) ty_sig * 'r * 's option -> ty_ml
Sourceval 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
Sourcetype '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.

    *)
Sourcetype 'a vernac_argument = {
  1. arg_printer : Environ.env -> Evd.evar_map -> 'a -> Pp.t;
  2. arg_parsing : 'a argument_rule;
}
Sourceval 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