Imported Upstream version 8.9.0upstream/8.9.0upstream

1 files changed, 6 insertions, 0 deletions

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