Add API Evd.mem_shelf instead of going through lower level Evd.shelf

Author: SkySkimmer

engine/evd.ml

@@ -1303,6 +1303,8 @@ let given_up evd = evd.given_up
 
 let shelf evd = List.flatten evd.shelf
 
+let mem_shelf e evd = List.exists (List.exists (fun e' -> Evar.equal e e')) evd.shelf
+
 let pr_shelf evd =
   let open Pp in
   if List.is_empty evd.shelf then str"(empty stack)"

engine/evd.mli

@@ -441,6 +441,10 @@ val unshelve : evar_map -> Evar.t list -> evar_map
 val given_up : evar_map -> Evar.Set.t
 
 val shelf : evar_map -> Evar.t list
+(** All evars in the shelf (not just the shallowest shelf) *)
+
+val mem_shelf : Evar.t -> evar_map -> bool
+(** [true] if the evar is in the shelf (not necessarily in the shallowest shelf) *)
 
 val pr_shelf : evar_map -> Pp.t
 

proofs/proof.ml

@@ -202,7 +202,7 @@ let focus_id cond inf id pr =
         (* goal is already under focus *)
         _focus cond inf i i pr
      | None ->
-        if CList.mem_f Evar.equal ev (Evd.shelf evar_map) then
+        if Evd.mem_shelf ev evar_map then
           (* goal is on the shelf, put it in focus *)
           let proofview = Proofview.unshelve [ev] pr.proofview in
           let pr = { pr with proofview } in

proofs/refine.ml

@@ -75,8 +75,7 @@ let generic_refine ~typecheck f gl =
   let future_goals, sigma = Evd.pop_future_goals sigma in
   (* Select the goals *)
   let future_goals = Evd.FutureGoals.map_filter (Proofview.Unsafe.advance sigma) future_goals in
-  let shelf = Evd.shelf sigma in
-  let future_goals = Evd.FutureGoals.filter (fun ev -> not @@ List.mem ev shelf) future_goals in
+  let future_goals = Evd.FutureGoals.filter (fun ev -> not @@ Evd.mem_shelf ev sigma) future_goals in
   (* Proceed to the refinement *)
   let sigma = match Proofview.Unsafe.advance sigma self with
   | None ->