package coq

  1. Overview
  2. Docs
package coq
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Vernacstate.DeclareSource

  • deprecated This module is internal and should not be used, instead, thread the proof state
Sourceexception NoCurrentProof
Sourceval there_are_pending_proofs : unit -> bool
Sourceval get_open_goals : unit -> int
Sourceval give_me_the_proof : unit -> Proof.t
Sourceval give_me_the_proof_opt : unit -> Proof.t option
Sourceval get_current_proof_name : unit -> Names.Id.t
Sourceval map_proof : (Proof.t -> Proof.t) -> unit
Sourceval with_current_proof : (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a
Sourceval return_proof : unit -> Declare.Proof.closed_proof_output
Sourceval return_partial_proof : unit -> Declare.Proof.closed_proof_output
Sourceval close_proof : opaque:Vernacexpr.opacity_flag -> keep_body_ucst_separate:bool -> Declare.Proof.proof_object
Sourceval discard_all : unit -> unit
Sourceval update_sigma_univs : UGraph.t -> unit
Sourceval get_current_context : unit -> Evd.evar_map * Environ.env
Sourceval get_all_proof_names : unit -> Names.Id.t list
Sourceval copy_terminators : src:LemmaStack.t option -> tgt:LemmaStack.t option -> LemmaStack.t option
Sourceval get : unit -> LemmaStack.t option
Sourceval get_program : unit -> Declare.OblState.t NeList.t
Sourceval set : (LemmaStack.t option * Declare.OblState.t NeList.t) -> unit
Sourceval get_pstate : unit -> Declare.Proof.t option
Sourceval freeze : marshallable:bool -> LemmaStack.t option
Sourceval unfreeze : LemmaStack.t -> unit
OCaml

Innovation. Community. Security.

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