1 files changed, 45 insertions, 0 deletions
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 51e0a1d6..8bbd82bb 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -63,6 +63,7 @@ exception CannotUnfocusThisWay
 (* Cannot focus on non-existing subgoals *)
 exception NoSuchGoals of int * int
 
+exception NoSuchGoal of Names.Id.t
 
 exception FullyUnfocused
 
@@ -75,6 +76,10 @@ let _ = CErrors.register_handler begin function
       CErrors.user_err ~hdr:"Focus" Pp.(
         str"Not every goal in range ["++ int i ++ str","++int j++str"] exist."
       )
+  | NoSuchGoal id ->
+      CErrors.user_err
+        ~hdr:"Focus"
+        Pp.(str "No such goal: " ++ str (Names.Id.to_string id) ++ str ".")
   | FullyUnfocused -> CErrors.user_err Pp.(str "The proof is not focused")
   | _ -> raise CErrors.Unhandled
 end
@@ -230,6 +235,37 @@ let focus cond inf i pr =
   try _focus cond (Obj.repr inf) i i pr
   with CList.IndexOutOfRange -> raise (NoSuchGoals (i,i))
 
+(* Focus on the goal named id *)
+let focus_id cond inf id pr =
+  let (focused_goals, evar_map) = Proofview.proofview pr.proofview in
+  begin match try Some (Evd.evar_key id evar_map) with Not_found -> None with
+  | Some ev ->
+     begin match CList.safe_index Evar.equal ev focused_goals with
+     | Some i ->
+        (* goal is already under focus *)
+        _focus cond (Obj.repr inf) i i pr
+     | None ->
+        if CList.mem_f Evar.equal ev pr.shelf then
+          (* goal is on the shelf, put it in focus *)
+          let proofview = Proofview.unshelve [ev] pr.proofview in
+          let shelf =
+            CList.filter (fun ev' -> Evar.equal ev ev' |> not) pr.shelf
+          in
+          let pr = { pr with proofview; shelf } in
+          let (focused_goals, _) = Proofview.proofview pr.proofview in
+          let i =
+            (* Now we know that this will succeed *)
+            try CList.index Evar.equal ev focused_goals
+            with Not_found -> assert false
+          in
+          _focus cond (Obj.repr inf) i i pr
+        else
+          raise CannotUnfocusThisWay
+     end
+  | None ->
+     raise (NoSuchGoal id)
+  end
+
 let rec unfocus kind pr () =
   let cond = cond_of_focus pr in
   match test_cond cond kind pr.proofview with
@@ -452,3 +488,12 @@ module V82 = struct
     { pr with proofview ; shelf }
 
 end
+
+let all_goals p =
+  let add gs set =
+    List.fold_left (fun s g -> Goal.Set.add g s) set gs in
+  let (goals,stack,shelf,given_up,_) = proof p in
+    let set = add goals Goal.Set.empty in
+    let set = List.fold_left (fun s gs -> let (g1, g2) = gs in add g1 (add g2 set)) set stack in
+    let set = add shelf set in
+    add given_up set