Merge PR #7825: [tactics] Refine test for unresolved evars: not reachable from initial evars

Ack-by: JasonGross
Ack-by: Zimmi48
Reviewed-by: ejgallego
Reviewed-by: gares
Ack-by: jfehrle
Ack-by: maximedenes
Reviewed-by: ppedrot

1 files changed, 5 insertions, 1 deletions

diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli
index 6cca3f5a5e..00d322858d 100644
--- a/engine/proofview_monad.mli
+++ b/engine/proofview_monad.mli
@@ -79,7 +79,7 @@ val with_empty_state : goal -> goal_with_state
 val map_goal_with_state : (goal -> goal) -> goal_with_state -> goal_with_state
 
 (** Type of proof views: current [evar_map] together with the list of
-    focused goals. *)
+    focused goals, locally shelved goals and globally shelved goals. *)
 type proofview = {
   solution : Evd.evar_map;
   comb : goal_with_state list;
@@ -115,6 +115,10 @@ module type State = sig
   val set : t -> unit Logical.t
   val modify : (t->t) -> unit Logical.t
 end
+module type Reader = sig
+  type t
+  val get : t Logical.t
+end
 
 module type Writer = sig
   type t