Module `Vernactypes`

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 = { inprog : 'inprog InProg.t; outprog : 'outprog InProg.t; inproof : 'inproof InProof.t; outproof : 'outproof OutProof.t; }
type typed_vernac = | TypedVernac : { inprog : 'inprog InProg.t; outprog : 'outprog OutProg.t; inproof : 'inproof InProof.t; outproof : 'outproof OutProof.t; run : pm:'inprog -> proof:'inproof -> 'outprog * 'outproof; } -> typed_vernac

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
val vtopenproofprogram : (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t) -> typed_vernac