From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 proofs/proof.mli | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'proofs/proof.mli')

diff --git a/proofs/proof.mli b/proofs/proof.mli
index c0e832fb..511dcc2e 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -137,6 +137,9 @@ val done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition
    a need for it? *)
 val focus : 'a focus_condition -> 'a -> int -> t -> t
 
+(* focus on goal named id *)
+val focus_id : 'aa focus_condition -> 'a -> Names.Id.t -> t -> t
+
 exception FullyUnfocused
 exception CannotUnfocusThisWay
 
@@ -207,3 +210,6 @@ module V82 : sig
   (* Implements the Existential command *)
   val instantiate_evar : int -> Constrexpr.constr_expr -> t -> t
 end
+
+(* returns the set of all goals in the proof *)
+val all_goals : t -> Goal.Set.t
-- 
cgit v1.2.3