package coq-core

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

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. Used by coqpp.

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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events Blog 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