summaryrefslogtreecommitdiff
path: root/proofs/proof.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proof.mli')
-rw-r--r--proofs/proof.mli14
1 files changed, 11 insertions, 3 deletions
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 12af18f4..715b3341 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -114,12 +114,18 @@ exception CannotUnfocusThisWay
is not met. *)
val unfocus : 'a focus_kind -> proof -> unit
+(* [unfocused p] returns [true] when [p] is fully unfocused. *)
+val unfocused : proof -> bool
+
(* [get_at_focus k] gets the information stored at the closest focus point
of kind [k].
Raises [NoSuchFocus] if there is no focus point of kind [k]. *)
exception NoSuchFocus
val get_at_focus : 'a focus_kind -> proof -> 'a
+(* [is_last_focus k] check if the most recent focus is of kind [k] *)
+val is_last_focus : 'a focus_kind -> proof -> bool
+
(* returns [true] if there is no goal under focus. *)
val no_focused_goal : proof -> bool
@@ -127,8 +133,6 @@ val no_focused_goal : proof -> bool
val get_proof_info : proof -> Store.t
-val set_proof_info : Store.t -> proof -> unit
-
(* Sets the section variables assumed by the proof *)
val set_used_variables : Sign.section_context -> proof -> unit
val get_used_variables : proof -> Sign.section_context option
@@ -151,7 +155,7 @@ val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> unit
a focusing command and a tactic. Transactions are such that if
any of the atomic action fails, the whole transaction fails.
- During a transaction, the undo visible undo stack is constituted only
+ During a transaction, the visible undo stack is constituted only
of the actions performed done during the transaction.
[transaction p f] can be called on an [f] using, itself, [transaction p].*)
@@ -178,6 +182,10 @@ module V82 : sig
(* returns the existential variable used to start the proof *)
val top_evars : proof -> Evd.evar list
+ (* Turns the unresolved evars into goals.
+ Raises [UnfinishedProof] if there are still unsolved goals. *)
+ val grab_evars : proof -> unit
+
(* Implements the Existential command *)
val instantiate_evar : int -> Topconstr.constr_expr -> proof -> unit
end