package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (3)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.0.1.tar.gz
sha256=051f7bf702ff0a3b370449728921e5a95e18bc2b31b8eb949d48422888c98af4

doc/rocq-runtime.vernac/Vernacstate/Declare/index.html

Module Vernacstate.DeclareSource

  • deprecated (8.11) 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 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_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 unfreeze : LemmaStack.t -> unit