package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

md5=13d2793fc6413aac5168822313e4864e

sha512=ec8379df34ba6e72bcf0218c66fef248b0e4c5c436fb3f2d7dd83a2c5f349dd0874a67484fcf9c0df3e5d5937d7ae2b2a79274725595b4b0065a381f70769b42

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

val 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

val close_future_proof : 
  feedback_id:Stateid.t ->
  Declare.Proof.closed_proof_output Future.computation ->
  Declare.Proof.proof_object

val 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

val 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