package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

Declare.Proof.t Construction of constants using interactive proofs.

type t
val start : info:Info.t -> cinfo:EConstr.t CInfo.t -> Evd.evar_map -> t

start_proof ~info ~cinfo sigma starts a proof of cinfo. The proof is started in the evar map sigma (which can typically contain universe constraints)

val start_derive : f:Names.Id.t -> name:Names.Id.t -> info:Info.t -> Proofview.telescope -> t

start_{derive,equations} are functions meant to handle interactive proofs with multiple goals, they should be considered experimental until we provide a more general API encompassing both of them. Please, get in touch with the developers if you would like to experiment with multi-goal dependent proofs so we can use your input on the design of the new API.

val start_with_initialization : info:Info.t -> cinfo:Constr.t CInfo.t -> Evd.evar_map -> t

Pretty much internal, used by the Lemma vernaculars

type mutual_info = bool * lemma_possible_guards * Constr.t option list option
val start_mutual_with_initialization : info:Info.t -> cinfo:Constr.t CInfo.t list -> mutual_info:mutual_info -> Evd.evar_map -> int list option -> t

Pretty much internal, used by mutual Lemma / Fixpoint vernaculars

val save : pm:OblState.t -> proof:t -> opaque:Vernacexpr.opacity_flag -> idopt:Names.lident option -> OblState.t * Names.GlobRef.t list

Qed a proof

val save_regular : proof:t -> opaque:Vernacexpr.opacity_flag -> idopt:Names.lident option -> Names.GlobRef.t list

For proofs known to have Regular ending, no need to touch program state.

val save_admitted : pm:OblState.t -> proof:t -> OblState.t

Admit a proof

val by : unit Proofview.tactic -> t -> t * bool

by tac applies tactic tac to the 1st subgoal of the current focused proof. Returns false if an unsafe tactic has been used.

val get : t -> Proof.t

Operations on ongoing proofs

val get_name : t -> Names.Id.t
val fold : f:(Proof.t -> 'a) -> t -> 'a
val map : f:(Proof.t -> Proof.t) -> t -> t
val map_fold : f:(Proof.t -> Proof.t * 'a) -> t -> t * 'a
val map_fold_endline : f:(unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> t -> t * 'a
val set_endline_tactic : Genarg.glob_generic_argument -> t -> t

Sets the tactic to be used when a tactic line is closed with ...

val definition_scope : t -> Locality.definition_scope
val set_used_variables : t -> using:Proof_using.t -> Constr.named_context * t

Sets the section variables assumed by the proof, returns its closure * (w.r.t. type dependencies and let-ins covered by it)

val get_used_variables : t -> Names.Id.Set.t option

Gets the set of variables declared to be used by the proof. None means no "Proof using" or #using was given

val compact : t -> t

Compacts the representation of the proof by pruning all intermediate terms

val update_sigma_univs : UGraph.t -> t -> t

Update the proof's universe information typically after a side-effecting command (e.g. a sublemma definition) has been run inside it.

val get_open_goals : t -> int
val get_recnames : t -> Names.Id.t list

Gets the set of mutual theorem names being currently built, if any

Helpers to obtain proof state when in an interactive proof

get_goal_context n returns the context of the nth subgoal of the current focused proof or raises a UserError if there is no focused proof or if there is no more subgoals

val get_goal_context : t -> int -> Evd.evar_map * Environ.env
val get_current_goal_context : t -> Evd.evar_map * Environ.env

get_current_goal_context () works as get_goal_context 1

val get_current_context : t -> Evd.evar_map * Environ.env

get_current_context () returns the context of the current focused goal. If there is no focused goal but there is a proof in progress, it returns the corresponding evar_map. If there is no pending proof then it returns the current global environment and empty evar_map.

Proof delay API, warning, internal, not stable

type closed_proof_output
val return_proof : t -> closed_proof_output

Requires a complete proof.

val return_partial_proof : t -> closed_proof_output

An incomplete proof is allowed (no error), and a warn is given if the proof is complete.

type proof_object

XXX: This is an internal, low-level API and could become scheduled for removal from the public API, use higher-level declare APIs instead

val close_proof : ?warn_incomplete:bool -> opaque:Vernacexpr.opacity_flag -> keep_body_ucst_separate:bool -> t -> proof_object
val close_future_proof : feedback_id:Stateid.t -> t -> closed_proof_output Future.computation -> proof_object
val save_lemma_admitted_delayed : pm:OblState.t -> proof:proof_object -> OblState.t

Special cases for delayed proofs, in this case we must provide the proof information so the proof won't be forced.

val save_lemma_proved_delayed : pm:OblState.t -> proof:proof_object -> idopt:Names.lident option -> OblState.t * Names.GlobRef.t list
val get_po_name : proof_object -> Names.Id.t

Used by the STM only to store info, should go away

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