Vernactypes (rocq-runtime.Vernactypes)

module Prog : sig ... end

module Proof : sig ... end

module OpaqueAccess : sig ... end

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

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

}

type no_state = (unit, unit, unit) state_gen

val no_state : no_state

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

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

type '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

type typed_vernac = unit typed_vernac_gen

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

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

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

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

val run : ?loc:Loc.t -> 'r typed_vernac_gen -> full_state -> full_state * 'r

Some convenient typed_vernac constructors. Used by coqpp.

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

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

val vtcloseproof : 
  ?check_late_init:bool ->
  (lemma:Declare.Proof.t -> pm:Declare.OblState.t -> Declare.OblState.t) ->
  typed_vernac

val vtopenproof : (unit -> Declare.Proof.t) -> typed_vernac

val vtmodifyproof : 
  ?check_late_init:bool ->
  (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

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