Vernactypes (p.rocq-runtime.9.0.0.doc.rocq-runtime.vernac.Vernactypes)

Sourcemodule Prog : sig ... end

Sourcemodule Proof : sig ... end

Sourcemodule OpaqueAccess : sig ... end

Sourcetype ('prog, 'proof, 'opaque_access) state_gen = {

prog : 'prog;
proof : 'proof;
opaque_access : 'opaque_access;

}

Sourcetype no_state = (unit, unit, unit) state_gen

Sourceval no_state : no_state

Useful for patterns like { no_state with proof = newproof } when modifying a subset of the state.

Source

val ignore_state : 
  ((unit, unit) Prog.t, (unit, unit) Proof.t, unit OpaqueAccess.t) state_gen

Sourcetype 'r typed_vernac_gen =

| TypedVernac : {
1. spec : (('inprog, 'outprog) Prog.t, ('inproof, 'outproof) Proof.t, 'inaccess OpaqueAccess.t) state_gen;
2. run : ('inprog, 'inproof, 'inaccess) state_gen -> ('outprog, 'outproof, unit) state_gen * 'r;
} -> 'r typed_vernac_gen

Sourcetype typed_vernac = unit typed_vernac_gen

Source

val typed_vernac_gen : 
  (('inprog, 'outprog) Prog.t,
    ('inproof, 'outproof) Proof.t,
    'inaccess OpaqueAccess.t)
    state_gen ->
  (('inprog, 'inproof, 'inaccess) state_gen ->
    ('outprog, 'outproof, unit) state_gen * 'r) ->
  'r typed_vernac_gen

Sourceval map_typed_vernac : ('a -> 'b) -> 'a typed_vernac_gen -> 'b typed_vernac_gen

Source

val typed_vernac : 
  (('inprog, 'outprog) Prog.t,
    ('inproof, 'outproof) Proof.t,
    'inaccess OpaqueAccess.t)
    state_gen ->
  (('inprog, 'inproof, 'inaccess) state_gen ->
    ('outprog, 'outproof, unit) state_gen) ->
  typed_vernac

Sourcetype full_state = (Prog.stack, Vernacstate.LemmaStack.t option, unit) state_gen

Sourceval run : 'r typed_vernac_gen -> full_state -> full_state * 'r

Some convenient typed_vernac constructors. Used by coqpp.

Sourceval vtdefault : (unit -> unit) -> typed_vernac

Sourceval vtnoproof : (unit -> unit) -> typed_vernac

Source

val vtcloseproof : 
  (lemma:Declare.Proof.t -> pm:Declare.OblState.t -> Declare.OblState.t) ->
  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

Source

val vtmodifyprogram : 
  (pm:Declare.OblState.t -> Declare.OblState.t) ->
  typed_vernac

Source

val vtdeclareprogram : 
  (pm:Declare.OblState.t -> Declare.Proof.t) ->
  typed_vernac

Source

val vtopenproofprogram : 
  (pm:Declare.OblState.t -> Declare.OblState.t * Declare.Proof.t) ->
  typed_vernac

Source

val vtopaqueaccess : 
  (opaque_access:Global.indirect_accessor -> unit) ->
  typed_vernac