diff options
Diffstat (limited to 'proofs/proof_global.mli')
-rw-r--r-- | proofs/proof_global.mli | 137 |
1 files changed, 137 insertions, 0 deletions
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli new file mode 100644 index 00000000..ed6a60c7 --- /dev/null +++ b/proofs/proof_global.mli @@ -0,0 +1,137 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** This module defines proof facilities relevant to the + toplevel. In particular it defines the global proof + environment. *) + +(** Type of proof modes : + - A name + - A function [set] to set it *from standard mode* + - A function [reset] to reset the *standard mode* from it + +*) +type proof_mode = { + name : string ; + set : unit -> unit ; + reset : unit -> unit +} + +(** Registers a new proof mode which can then be adressed by name + in [set_default_proof_mode]. + One mode is already registered - the standard mode - named "No", + It corresponds to Coq default setting are they are set when coqtop starts. *) +val register_proof_mode : proof_mode -> unit + +val there_is_a_proof : unit -> bool +val there_are_pending_proofs : unit -> bool +val check_no_pending_proof : unit -> unit + +val get_current_proof_name : unit -> Names.identifier +val get_all_proof_names : unit -> Names.identifier list + +val discard : Names.identifier Util.located -> unit +val discard_current : unit -> unit +val discard_all : unit -> unit + +(** [set_proof_mode] sets the proof mode to be used after it's called. It is + typically called by the Proof Mode command. *) +val set_proof_mode : string -> unit + +exception NoCurrentProof +val give_me_the_proof : unit -> Proof.proof + + +(** [start_proof s str goals ~init_tac ~compute_guard hook] starts + a proof of name [s] and + conclusion [t]; [hook] is optionally a function to be applied at + proof end (e.g. to declare the built constructions as a coercion + or a setoid morphism). *) +type lemma_possible_guards = int list list +val start_proof : Names.identifier -> + Decl_kinds.goal_kind -> + (Environ.env * Term.types) list -> + ?compute_guard:lemma_possible_guards -> + Tacexpr.declaration_hook -> + unit + +val close_proof : unit -> + Names.identifier * + (Entries.definition_entry list * + lemma_possible_guards * + Decl_kinds.goal_kind * + Tacexpr.declaration_hook) + +exception NoSuchProof + +val suspend : unit -> unit +val resume_last : unit -> unit + +val resume : Names.identifier -> unit +(** @raise NoSuchProof if it doesn't find one. *) + +(** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is + no current proof. *) +val run_tactic : unit Proofview.tactic -> unit + +(** Sets the tactic to be used when a tactic line is closed with [...] *) +val set_endline_tactic : unit Proofview.tactic -> unit + +(** Sets the section variables assumed by the proof *) +val set_used_variables : Names.identifier list -> unit +val get_used_variables : unit -> Sign.section_context option + +(** Appends the endline tactic of the current proof to a tactic. *) +val with_end_tac : unit Proofview.tactic -> unit Proofview.tactic + +(**********************************************************) +(* *) +(* Utility functions *) +(* *) +(**********************************************************) + +(** [maximal_unfocus k p] unfocuses [p] until [p] has at least a + focused goal or that the last focus isn't of kind [k]. *) +val maximal_unfocus : 'a Proof.focus_kind -> Proof.proof -> unit + +(**********************************************************) +(* *) +(* Bullets *) +(* *) +(**********************************************************) + +module Bullet : sig + type t = Vernacexpr.bullet + + (** A [behavior] is the data of a put function which + is called when a bullet prefixes a tactic, together + with a name to identify it. *) + type behavior = { + name : string; + put : Proof.proof -> t -> unit + } + + (** A registered behavior can then be accessed in Coq + through the command [Set Bullet Behavior "name"]. + + Two modes are registered originally: + * "Strict Subproofs": + - If this bullet follows another one of its kind, defocuses then focuses + (which fails if the focused subproof is not complete). + - If it is the first bullet of its kind, then focuses a new subproof. + * "None": bullets don't do anything *) + val register_behavior : behavior -> unit + + (** Handles focusing/defocusing with bullets: + *) + val put : Proof.proof -> t -> unit +end + +module V82 : sig + val get_current_initial_conclusions : unit -> Names.identifier *(Term.types list * Decl_kinds.goal_kind * Tacexpr.declaration_hook) +end |