Cleanup evar_extra: remove evar_info's store and add maps to evar_map

24 files changed, 214 insertions, 201 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index f9d9ce3569..69830960a9 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -410,7 +410,7 @@ let new_pure_evar_full evd evi =
   let evd = Evd.declare_future_goal evk evd in
   (evd, evk)
 
-let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) sign evd typ =
+let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?naming ?(principal=false) sign evd typ =
   let default_naming = IntroAnonymous in
   let naming = Option.default default_naming naming in
   let name = match naming with
@@ -427,8 +427,7 @@ let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?
     evar_body = Evar_empty;
     evar_filter = filter;
     evar_source = src;
-    evar_candidates = candidates;
-    evar_extra = store; }
+    evar_candidates = candidates }
   in
   let (evd, newevk) = Evd.new_evar evd ?name evi in
   let evd =
@@ -437,24 +436,24 @@ let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?
   in
   (evd, newevk)
 
-let new_evar_instance ?src ?filter ?candidates ?store ?naming ?principal sign evd typ instance =
+let new_evar_instance ?src ?filter ?candidates ?naming ?principal sign evd typ instance =
   let open EConstr in
   assert (not !Flags.debug ||
             List.distinct (ids_of_named_context (named_context_of_val sign)));
-  let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in
+  let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?naming ?principal typ in
   evd, mkEvar (newevk,Array.of_list instance)
 
-let new_evar_from_context ?src ?filter ?candidates ?store ?naming ?principal sign evd typ =
+let new_evar_from_context ?src ?filter ?candidates ?naming ?principal sign evd typ =
   let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
   let instance =
     match filter with
     | None -> instance
     | Some filter -> Filter.filter_list filter instance in
-  new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance
+  new_evar_instance sign evd typ ?src ?filter ?candidates ?naming ?principal instance
 
 (* [new_evar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
-let new_evar ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming env evd typ =
+let new_evar ?src ?filter ?candidates ?naming ?principal ?hypnaming env evd typ =
   let sign,typ',instance,subst = push_rel_context_to_named_context ?hypnaming env evd typ in
   let map c = csubst_subst subst c in
   let candidates = Option.map (fun l -> List.map map l) candidates in
@@ -462,7 +461,7 @@ let new_evar ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming env e
     match filter with
     | None -> instance
     | Some filter -> Filter.filter_list filter instance in
-  new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance
+  new_evar_instance sign evd typ' ?src ?filter ?candidates ?naming ?principal instance
 
 let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid =
   let (evd', s) = new_sort_variable rigid evd in
@@ -714,7 +713,7 @@ let rec advance sigma evk =
   match evi.evar_body with
   | Evar_empty -> Some evk
   | Evar_defined v ->
-      match is_restricted_evar evi with
+      match is_restricted_evar sigma evk with
       | Some evk -> advance sigma evk
       | None -> None
 
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 11e07175e3..49443164cc 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -27,7 +27,7 @@ val mk_new_meta : unit -> constr
 
 val new_evar_from_context :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
-  ?candidates:constr list -> ?store:Store.t ->
+  ?candidates:constr list ->
   ?naming:intro_pattern_naming_expr ->
   ?principal:bool ->
   named_context_val -> evar_map  -> types -> evar_map * EConstr.t
@@ -40,14 +40,14 @@ type naming_mode =
 
 val new_evar :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
-  ?candidates:constr list -> ?store:Store.t ->
+  ?candidates:constr list ->
   ?naming:intro_pattern_naming_expr ->
   ?principal:bool -> ?hypnaming:naming_mode ->
   env -> evar_map -> types -> evar_map * EConstr.t
 
 val new_pure_evar :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
-  ?candidates:constr list -> ?store:Store.t ->
+  ?candidates:constr list ->
   ?naming:intro_pattern_naming_expr ->
   ?principal:bool ->
   named_context_val -> evar_map -> types -> evar_map * Evar.t
@@ -77,7 +77,7 @@ val new_global : evar_map -> GlobRef.t -> evar_map * constr
    as a telescope) is [sign] *)
 val new_evar_instance :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list ->
-  ?store:Store.t -> ?naming:intro_pattern_naming_expr ->
+  ?naming:intro_pattern_naming_expr ->
   ?principal:bool ->
  named_context_val -> evar_map -> types ->
   constr list -> evar_map * constr
diff --git a/engine/evd.ml b/engine/evd.ml
index eafdc4cb46..3a01706063 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -144,8 +144,7 @@ type evar_info = {
   evar_body : evar_body;
   evar_filter : Filter.t;
   evar_source : Evar_kinds.t Loc.located;
-  evar_candidates : constr list option; (* if not None, list of allowed instances *)
-  evar_extra : Store.t }
+  evar_candidates : constr list option; (* if not None, list of allowed instances *)}
 
 let make_evar hyps ccl = {
   evar_concl = ccl;
@@ -153,9 +152,7 @@ let make_evar hyps ccl = {
   evar_body = Evar_empty;
   evar_filter = Filter.identity;
   evar_source = Loc.tag @@ Evar_kinds.InternalHole;
-  evar_candidates = None;
-  evar_extra = Store.empty
-}
+  evar_candidates = None; }
 
 let instance_mismatch () =
   anomaly (Pp.str "Signature and its instance do not match.")
@@ -413,6 +410,11 @@ end
 
 type goal_kind = ToShelve | ToGiveUp
 
+type evar_flags =
+  { obligation_evars : Evar.Set.t;
+    restricted_evars : Evar.t Evar.Map.t;
+    unresolvable_evars : Evar.Set.t }
+
 type evar_map = {
   (** Existential variables *)
   defn_evars : evar_info EvMap.t;
@@ -425,6 +427,7 @@ type evar_map = {
   last_mods  : Evar.Set.t;
   (** Metas *)
   metas      : clbinding Metamap.t;
+  evar_flags : evar_flags;
   (** Interactive proofs *)
   effects    : Safe_typing.private_constants;
   future_goals : Evar.t list; (** list of newly created evars, to be
@@ -456,6 +459,45 @@ let add_with_name ?name d e i = match i.evar_body with
 
 let add d e i = add_with_name d e i
 
+(*** Evar flags: resolvable, restricted or obligation flag *)
+
+let set_resolvable_evar evd evk b =
+  let flags = evd.evar_flags in
+  let unresolvable_evars = flags.unresolvable_evars in
+  let unresolvable_evars =
+    if b then Evar.Set.remove evk unresolvable_evars
+    else Evar.Set.add evk unresolvable_evars
+  in
+  { evd with evar_flags = { flags with unresolvable_evars } }
+
+let is_resolvable_evar evd evk =
+  let flags = evd.evar_flags in
+  not (Evar.Set.mem evk flags.unresolvable_evars)
+
+let inherit_unresolvable_evar evar_flags evk evk' =
+  let evk_unres = Evar.Set.mem evk evar_flags.unresolvable_evars in
+  let unresolvable_evars = Evar.Set.remove evk evar_flags.unresolvable_evars in
+  let unresolvable_evars =
+    if evk_unres then Evar.Set.add evk' unresolvable_evars else unresolvable_evars
+  in { evar_flags with unresolvable_evars }
+
+let unresolvable_evars evd = evd.evar_flags.unresolvable_evars
+
+let set_obligation_evar evd evk =
+  let flags = evd.evar_flags in
+  let evar_flags = { flags with obligation_evars = Evar.Set.add evk flags.obligation_evars } in
+  { evd with evar_flags }
+
+let is_obligation_evar evd evk =
+  let flags = evd.evar_flags in
+  Evar.Set.mem evk flags.obligation_evars
+
+let remove_evar_flags evk evar_flags =
+  { unresolvable_evars = Evar.Set.remove evk evar_flags.unresolvable_evars;
+    obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars;
+    (** Restriction information is kept. *)
+    restricted_evars = evar_flags.restricted_evars }
+
 (** New evars *)
 
 let evar_counter_summary_name = "evar counter"
@@ -478,7 +520,9 @@ let remove d e =
   in
   let future_goals = List.filter (fun e' -> not (Evar.equal e e')) d.future_goals in
   let future_goals_status = EvMap.remove e d.future_goals_status in
-  { d with undf_evars; defn_evars; principal_future_goal; future_goals; future_goals_status }
+  let evar_flags = remove_evar_flags e d.evar_flags in
+  { d with undf_evars; defn_evars; principal_future_goal; future_goals; future_goals_status;
+           evar_flags }
 
 let find d e =
   try EvMap.find e d.undf_evars
@@ -583,12 +627,18 @@ let cmap f evd =
 let create_evar_defs sigma = { sigma with
   conv_pbs=[]; last_mods=Evar.Set.empty; metas=Metamap.empty }
 
+let empty_evar_flags =
+  { obligation_evars = Evar.Set.empty;
+    restricted_evars = Evar.Map.empty;
+    unresolvable_evars = Evar.Set.empty }
+
 let empty = {
   defn_evars = EvMap.empty;
   undf_evars = EvMap.empty;
   universes  = UState.empty;
   conv_pbs   = [];
   last_mods  = Evar.Set.empty;
+  evar_flags = empty_evar_flags;
   metas      = Metamap.empty;
   effects    = Safe_typing.empty_private_constants;
   evar_names = EvNames.empty; (* id<->key for undefined evars *)
@@ -634,9 +684,7 @@ let evar_source evk d = (find d evk).evar_source
 let evar_ident evk evd = EvNames.ident evk evd.evar_names
 let evar_key id evd = EvNames.key id evd.evar_names
 
-let restricted = Store.field ()
-
-let define_aux ?dorestrict def undef evk body =
+let define_aux def undef evk body =
   let oldinfo =
     try EvMap.find evk undef
     with Not_found ->
@@ -646,10 +694,7 @@ let define_aux ?dorestrict def undef evk body =
         anomaly ~label:"Evd.define" (Pp.str "cannot define undeclared evar.")
   in
   let () = assert (oldinfo.evar_body == Evar_empty) in
-  let evar_extra = match dorestrict with
-    | Some evk' -> Store.set oldinfo.evar_extra restricted evk'
-    | None -> oldinfo.evar_extra in
-  let newinfo = { oldinfo with evar_body = Evar_defined body; evar_extra } in
+  let newinfo = { oldinfo with evar_body = Evar_defined body } in
   EvMap.add evk newinfo def, EvMap.remove evk undef
 
 (* define the existential of section path sp as the constr body *)
@@ -660,10 +705,15 @@ let define evk body evd =
   | _ -> Evar.Set.add evk evd.last_mods
   in
   let evar_names = EvNames.remove_name_defined evk evd.evar_names in
-  { evd with defn_evars; undf_evars; last_mods; evar_names }
+  let evar_flags = remove_evar_flags evk evd.evar_flags in
+  { evd with defn_evars; undf_evars; last_mods; evar_names; evar_flags }
+
+let is_restricted_evar evd evk =
+  try Some (Evar.Map.find evk evd.evar_flags.restricted_evars)
+  with Not_found -> None
 
-let is_restricted_evar evi =
-  Store.get evi.evar_extra restricted
+let declare_restricted_evar evar_flags evk evk' =
+  { evar_flags with restricted_evars = Evar.Map.add evk evk' evar_flags.restricted_evars }
 
 let restrict evk filter ?candidates ?src evd =
   let evk' = new_untyped_evar () in
@@ -679,9 +729,11 @@ let restrict evk filter ?candidates ?src evd =
   let ctxt = Filter.filter_list filter (evar_context evar_info) in
   let id_inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in
   let body = mkEvar(evk',id_inst) in
-  let (defn_evars, undf_evars) = define_aux ~dorestrict:evk' evd.defn_evars evd.undf_evars evk body in
+  let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
+  let evar_flags = declare_restricted_evar evd.evar_flags evk evk' in
+  let evar_flags = inherit_unresolvable_evar evar_flags evk evk' in
   { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
-    defn_evars; last_mods; evar_names }, evk'
+    defn_evars; last_mods; evar_names; evar_flags }, evk'
 
 let downcast evk ccl evd =
   let evar_info = EvMap.find evk evd.undf_evars in
@@ -1019,6 +1071,7 @@ let set_metas evd metas = {
   universes  = evd.universes;
   conv_pbs = evd.conv_pbs;
   last_mods = evd.last_mods;
+  evar_flags = evd.evar_flags;
   metas;
   effects = evd.effects;
   evar_names = evd.evar_names;
diff --git a/engine/evd.mli b/engine/evd.mli
index 1a5614988d..87f74f660d 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -83,10 +83,6 @@ type evar_body =
   | Evar_empty
   | Evar_defined of econstr
 
-
-module Store : Store.S
-(** Datatype used to store additional information in evar maps. *)
-
 type evar_info = {
   evar_concl : econstr;
   (** Type of the evar. *)
@@ -102,8 +98,6 @@ type evar_info = {
   (** Information about the evar. *)
   evar_candidates : econstr list option;
   (** List of possible solutions when known that it is a finite list *)
-  evar_extra : Store.t
-  (** Extra store, used for clever hacks. *)
 }
 
 val make_evar : named_context_val -> etypes -> evar_info
@@ -247,9 +241,24 @@ val restrict : Evar.t-> Filter.t -> ?candidates:econstr list ->
     possibly limiting the instances to a set of candidates (candidates
     are filtered according to the filter) *)
 
-val is_restricted_evar : evar_info -> Evar.t option
+val is_restricted_evar : evar_map -> Evar.t -> Evar.t option
 (** Tell if an evar comes from restriction of another evar, and if yes, which *)
 
+val set_resolvable_evar : evar_map -> Evar.t -> bool -> evar_map
+(** Declare an evar resolvable or unresolvable for typeclass resolution *)
+
+val unresolvable_evars : evar_map -> Evar.Set.t
+(** The set of unresolvable evars *)
+
+val is_resolvable_evar : evar_map -> Evar.t -> bool
+(** Is the evar declared resolvable for typeclass resolution *)
+
+val set_obligation_evar : evar_map -> Evar.t -> evar_map
+(** Declare an evar as an obligation *)
+
+val is_obligation_evar : evar_map -> Evar.t -> bool
+(** Is the evar declared as an obligation *)
+
 val downcast : Evar.t-> etypes -> evar_map -> evar_map
 (** Change the type of an undefined evar to a new type assumed to be a
     subtype of its current type; subtyping must be ensured by caller *)
@@ -357,6 +366,9 @@ val add_universe_constraints : evar_map -> UnivProblem.Set.t -> evar_map
 
 *)
 
+module Store : Store.S
+(** Datatype used to store additional information in evar maps. *)
+
 val get_extra_data : evar_map -> Store.t
 val set_extra_data : Store.t -> evar_map -> evar_map
 
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 12d31e5f46..aabc629ee4 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -60,20 +60,18 @@ type telescope =
   | TNil of Evd.evar_map
   | TCons of Environ.env * Evd.evar_map * EConstr.types * (Evd.evar_map -> EConstr.constr -> telescope)
 
-let typeclass_resolvable = Evd.Store.field ()
-
 let dependent_init =
-  (* Goals are created with a store which marks them as unresolvable
-     for type classes. *)
-  let store = Evd.Store.set Evd.Store.empty typeclass_resolvable () in
   (* Goals don't have a source location. *)
   let src = Loc.tag @@ Evar_kinds.GoalEvar in
   (* Main routine *)
   let rec aux = function
   | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] }
   | TCons (env, sigma, typ, t) ->
-    let (sigma, econstr) = Evarutil.new_evar env sigma ~src ~store typ in
+    let (sigma, econstr) = Evarutil.new_evar env sigma ~src typ in
     let (gl, _) = EConstr.destEvar sigma econstr in
+    (* Goals are created with a store which marks them as unresolvable
+       for type classes. *)
+    let sigma = Evd.set_resolvable_evar sigma gl false in
     let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
     let entry = (econstr, typ) :: ret in
     entry, { solution = sol; comb = with_empty_state gl :: comb; shelf = [] }
@@ -760,11 +758,8 @@ let mark_in_evm ~goal evd content =
             | loc,_ -> loc,Evar_kinds.GoalEvar }
     else info
   in
-  let info = match Evd.Store.get info.Evd.evar_extra typeclass_resolvable with
-  | None -> { info with Evd.evar_extra = Evd.Store.set info.Evd.evar_extra typeclass_resolvable () }
-  | Some () -> info
-  in
-  Evd.add evd content info
+  let evd = Evd.add evd content info in
+  Evd.set_resolvable_evar evd content false
 
 let with_shelf tac =
   let open Proof in
@@ -1045,8 +1040,6 @@ module Unsafe = struct
   let mark_as_unresolvable p gl =
     { p with solution = mark_in_evm ~goal:false p.solution gl }
 
-  let typeclass_resolvable = typeclass_resolvable
-
 end
 
 module UnsafeRepr = Proof.Unsafe
@@ -1065,10 +1058,6 @@ let goal_nf_evar sigma gl =
   let sigma = Evd.add sigma gl evi in
   (gl, sigma)
 
-let goal_extra evars gl =
-  let evi = Evd.find evars gl in
-  evi.Evd.evar_extra
-
 
 let catchable_exception = function
   | Logic_monad.Exception _ -> false
@@ -1093,7 +1082,6 @@ module Goal = struct
   let sigma {sigma} = sigma
   let hyps {env} = EConstr.named_context env
   let concl {concl} = concl
-  let extra {sigma; self} = goal_extra sigma self
 
   let gmake_with info env sigma goal state =
     { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ;
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 0bb3229a9b..7bf6390f0e 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -475,8 +475,6 @@ module Unsafe : sig
   val undefined : Evd.evar_map -> Proofview_monad.goal_with_state list ->
     Proofview_monad.goal_with_state list
 
-  val typeclass_resolvable : unit Evd.Store.field
-
 end
 
 (** This module gives access to the innards of the monad. Its use is
@@ -507,7 +505,6 @@ module Goal : sig
   val hyps : t -> named_context
   val env : t -> Environ.env
   val sigma : t -> Evd.evar_map
-  val extra : t -> Evd.Store.t
   val state : t -> Proofview_monad.StateStore.t
 
   (** [nf_enter t] applies the goal-dependent tactic [t] in each goal
diff --git a/engine/termops.ml b/engine/termops.ml
index e1f5fb0d7f..c4b57e4dd2 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -365,12 +365,18 @@ let pr_evar_map_gen with_univs pr_evars sigma =
     else
     str "CONSTRAINTS:" ++ brk (0, 1) ++
       pr_evar_constraints sigma conv_pbs ++ fnl ()
+  and unresolvables =
+    let evars = Evd.unresolvable_evars sigma in
+    if Evar.Set.is_empty evars then mt ()
+    else
+      str "UNRESOLVABLE:" ++ brk (0, 1) ++
+      prlist_with_sep spc (pr_existential_key sigma) (Evar.Set.elements evars) ++ fnl ()
   and metas =
     if List.is_empty (Evd.meta_list sigma) then mt ()
     else
       str "METAS:" ++ brk (0, 1) ++ pr_meta_map sigma
   in
-  evs ++ svs ++ cstrs ++ metas
+  evs ++ svs ++ cstrs ++ unresolvables ++ metas
 
 let pr_evar_list sigma l =
   let open Evd in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 9dd98a4ab7..8cecf9bd9b 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -89,9 +89,9 @@ let goalevars evars = fst evars
 let cstrevars evars = snd evars
 
 let new_cstr_evar (evd,cstrs) env t =
-  let s = Typeclasses.set_resolvable Evd.Store.empty false in
-  let (evd', t) = Evarutil.new_evar ~store:s env evd t in
+  let (evd', t) = Evarutil.new_evar env evd t in
   let ev, _ = destEvar evd' t in
+  let evd' = Evd.set_resolvable_evar evd' ev false in
     (evd', Evar.Set.add ev cstrs), t
 
 (** Building or looking up instances. *)
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 8dbef47fe1..a2dce621d9 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -164,7 +164,7 @@ let ltac_call tac (args:glob_tactic_arg list) =
 
 let dummy_goal env sigma =
   let (gl,_,sigma) = 
-    Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp Evd.Store.empty in
+    Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp in
   {Evd.it = gl; Evd.sigma = sigma}
 
 let constr_of evd v = match Value.to_constr v with
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 6746eff223..70a2a30cd5 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1365,7 +1365,7 @@ let tacTYPEOF c = Goal.enter_one ~__LOC__ (fun g ->
 
 (** This tactic creates a partial proof realizing the introduction rule, but
     does not check anything. *)
-let unsafe_intro env store decl b =
+let unsafe_intro env decl b =
   let open Context.Named.Declaration in
   Refine.refine ~typecheck:false begin fun sigma ->
     let ctx = Environ.named_context_val env in
@@ -1374,7 +1374,7 @@ let unsafe_intro env store decl b =
     let ninst = EConstr.mkRel 1 :: inst in
     let nb = EConstr.Vars.subst1 (EConstr.mkVar (get_id decl)) b in
     let sigma, ev =
-      Evarutil.new_evar_instance nctx sigma nb ~principal:true ~store ninst in
+      Evarutil.new_evar_instance nctx sigma nb ~principal:true ninst in
     sigma, EConstr.mkNamedLambda_or_LetIn decl ev
   end
 
@@ -1418,7 +1418,7 @@ let-in even after reduction, it fails. In case of success, the original name
 and final id are passed to the continuation [k] which gets evaluated. *)
 let tclINTRO ~id ~conclusion:k = Goal.enter begin fun gl ->
   let open Context in
-  let env, sigma, extra, g = Goal.(env gl, sigma gl, extra gl, concl gl) in
+  let env, sigma, g = Goal.(env gl, sigma gl, concl gl) in
   let decl, t, no_red = decompose_assum env sigma g in
   let original_name = Rel.Declaration.get_name decl in
   let already_used = Tacmach.New.pf_ids_of_hyps gl in
@@ -1433,7 +1433,7 @@ let tclINTRO ~id ~conclusion:k = Goal.enter begin fun gl ->
   in
   if List.mem id already_used then
     errorstrm Pp.(Id.print id ++ str" already used");
-  unsafe_intro env extra (set_decl_id id decl) t <*>
+  unsafe_intro env (set_decl_id id decl) t <*>
   (if no_red then tclUNIT () else tclFULL_BETAIOTA) <*>
   k ~orig_name:original_name ~new_name:id
 end
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 4a63dd4708..ebba6223b7 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -1045,7 +1045,7 @@ let thin id sigma goal =
   match ans with
   | None -> sigma
   | Some (sigma, hyps, concl) ->
-    let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in
+    let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl in
     let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
     sigma
 
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 22f438c00c..9422a96f21 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1238,19 +1238,26 @@ let check_evar_instance evd evk1 body conv_algo =
   | Success evd -> evd
   | UnifFailure _ -> raise (IllTypedInstance (evenv,ty, evi.evar_concl))
 
-let update_evar_source ev1 ev2 evd =
+let update_evar_info ev1 ev2 evd =
   let loc, evs2 = evar_source ev2 evd in
-  match evs2 with
-  | (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) ->
-     let evi = Evd.find evd ev1 in
-     Evd.add evd ev1 {evi with evar_source = loc, evs2}
-  | _ -> evd
-  
+  let evd =
+    (* We keep the obligation evar flag during evar-evar unifications *)
+    if is_obligation_evar evd ev2 then
+      let evi = Evd.find evd ev1 in
+      let evd = Evd.add evd ev1 {evi with evar_source = loc, evs2} in
+      Evd.set_obligation_evar evd ev1
+    else evd
+  in
+  (** [ev1] inherits the unresolvability status from [ev2] *)
+  if not (Evd.is_resolvable_evar evd ev2) then
+    Evd.set_resolvable_evar evd ev1 false
+  else evd
+
 let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) =
   try
     let evd,body = project_evar_on_evar force g env evd aliases 0 pbty ev1 ev2 in
     let evd' = Evd.define evk2 body evd in
-    let evd' = update_evar_source (fst (destEvar evd body)) evk2 evd' in
+    let evd' = update_evar_info (fst (destEvar evd body)) evk2 evd' in
       check_evar_instance evd' evk2 body g
   with EvarSolvedOnTheFly (evd,c) ->
     f env evd pbty ev2 c
@@ -1258,13 +1265,9 @@ let solve_evar_evar_l2r force f g env evd aliases pbty ev1 (evk2,_ as ev2) =
 let opp_problem = function None -> None | Some b -> Some (not b)
 
 let preferred_orientation evd evk1 evk2 =
-  let _,src1 = (Evd.find_undefined evd evk1).evar_source in
-  let _,src2 = (Evd.find_undefined evd evk2).evar_source in
-  (* This is a heuristic useful for program to work *)
-  match src1,src2 with
-  | (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) , _ -> true
-  | _, (Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_, _, false)) -> false
-  | _ -> true
+  if is_obligation_evar evd evk1 then true
+  else if is_obligation_evar evd evk2 then false
+  else true
 
 let solve_evar_evar_aux force f g env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
   let aliases = make_alias_map env evd in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index f2881e4a19..37afcf75e1 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -510,6 +510,15 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma
         | Some ty -> sigma, ty
         | None -> new_type_evar env sigma loc in
       let sigma, uj_val = new_evar env sigma ~src:(loc,k) ~naming ty in
+      let sigma =
+        if Flags.is_program_mode () then
+          match k with
+          | Evar_kinds.QuestionMark _
+          | Evar_kinds.ImplicitArg (_, _, false) ->
+            Evd.set_obligation_evar sigma (fst (destEvar sigma uj_val))
+          | _ -> sigma
+        else sigma
+      in
       sigma, { uj_val; uj_type = ty }
 
   | GHole (k, _naming, Some arg) ->
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 0bc35e5358..07821f03e5 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -481,37 +481,10 @@ let instances r =
 let is_class gr = 
   GlobRef.Map.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes
 
-(* To embed a boolean for resolvability status.
-   This is essentially a hack to mark which evars correspond to
-   goals and do not need to be resolved when we have nested [resolve_all_evars]
-   calls (e.g. when doing apply in an External hint in typeclass_instances).
-   Would be solved by having real evars-as-goals.
-
-   Nota: we will only check the resolvability status of undefined evars.
- *)
-
-let resolvable = Proofview.Unsafe.typeclass_resolvable
-
-let set_resolvable s b =
-  if b then Store.remove s resolvable
-  else Store.set s resolvable ()
-
-let is_resolvable evi =
-  assert (match evi.evar_body with Evar_empty -> true | _ -> false);
-  Option.is_empty (Store.get evi.evar_extra resolvable)
-
-let mark_resolvability_undef b evi =
-  if is_resolvable evi == (b : bool) then evi
-  else
-    let t = set_resolvable evi.evar_extra b in
-    { evi with evar_extra = t }
-
-let mark_resolvability b evi =
-  assert (match evi.evar_body with Evar_empty -> true | _ -> false);
-  mark_resolvability_undef b evi
-
-let mark_unresolvable evi = mark_resolvability false evi
-let mark_resolvable evi = mark_resolvability true evi
+let mark_resolvability_undef evm evk b =
+  let resolvable = Evd.is_resolvable_evar evm evk in
+  if b == resolvable then evm
+  else Evd.set_resolvable_evar evm evk b
 
 open Evar_kinds
 type evar_filter = Evar.t -> Evar_kinds.t -> bool
@@ -524,18 +497,18 @@ let no_goals_or_obligations _ = function
   | _ -> true
 
 let mark_resolvability filter b sigma =
-  let map ev evi =
-    if filter ev (snd evi.evar_source) then mark_resolvability_undef b evi
-    else evi
+  let map ev evi evm =
+    if filter ev (snd evi.evar_source) then mark_resolvability_undef evm ev b
+    else evm
   in
-  Evd.raw_map_undefined map sigma
+  Evd.fold_undefined map sigma sigma
 
 let mark_unresolvables ?(filter=all_evars) sigma = mark_resolvability filter false sigma
 let mark_resolvables ?(filter=all_evars) sigma = mark_resolvability filter true sigma
 
 let has_typeclasses filter evd =
   let check ev evi =
-    filter ev (snd evi.evar_source) && is_resolvable evi && is_class_evar evd evi
+    filter ev (snd evi.evar_source) && Evd.is_resolvable_evar evd ev && is_class_evar evd evi
   in
   Evar.Map.exists check (Evd.undefined_map evd)
 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index f0437be4ed..de9a99a868 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -107,12 +107,9 @@ val no_goals_or_obligations : evar_filter
     An unresolvable evar is an evar the type-class engine will NOT try to solve
 *)
 
-val set_resolvable : Evd.Store.t -> bool -> Evd.Store.t
-val is_resolvable : evar_info -> bool
-val mark_unresolvable : evar_info -> evar_info
 val mark_unresolvables : ?filter:evar_filter -> evar_map -> evar_map
 val mark_resolvables   : ?filter:evar_filter -> evar_map -> evar_map
-val mark_resolvable : evar_info -> evar_info
+
 val is_class_evar : evar_map -> evar_info -> bool
 val is_class_type : evar_map -> EConstr.types -> bool
 
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 95e908c4dd..7ebc789aa5 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -608,8 +608,8 @@ let make_evar_clause env sigma ?len t =
     else match EConstr.kind sigma t with
     | Cast (t, _, _) -> clrec (sigma, holes) n t
     | Prod (na, t1, t2) ->
-      let store = Typeclasses.set_resolvable Evd.Store.empty false in
-      let (sigma, ev) = new_evar ~store env sigma t1 in
+      let (sigma, ev) = new_evar env sigma t1 in
+      let sigma = Evd.set_resolvable_evar sigma (fst (destEvar sigma ev)) false in
       let dep = not (noccurn sigma 1 t2) in
       let hole = {
         hole_evar = ev;
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index ba4cde6d67..929443a969 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -65,8 +65,8 @@ let clenv_pose_dependent_evars ?(with_evars=false) clenv =
 (** Use our own fast path, more informative than from Typeclasses *)
 let check_tc evd =
   let has_resolvable = ref false in
-  let check _ evi =
-    let res = Typeclasses.is_resolvable evi in
+  let check ev evi =
+    let res = Evd.is_resolvable_evar evd ev in
     if res then
       let () = has_resolvable := true in
       Typeclasses.is_class_evar evd evi
diff --git a/proofs/goal.ml b/proofs/goal.ml
index c14c0a8a77..6aff43f741 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -50,13 +50,8 @@ module V82 = struct
     let evi = Evd.find evars gl in
     evi.Evd.evar_concl
 
-  (* Access to ".evar_extra" *)
-  let extra evars gl =
-    let evi = Evd.find evars gl in
-    evi.Evd.evar_extra
-
   (* Old style mk_goal primitive *)
-  let mk_goal evars hyps concl extra =
+  let mk_goal evars hyps concl =
     (* A goal created that way will not be used by refine and will not
        be shelved. It must not appear as a future_goal, so the future
        goals are restored to their initial value after the evar is
@@ -67,11 +62,10 @@ module V82 = struct
 		Evd.evar_filter = Evd.Filter.identity;
 		Evd.evar_body = Evd.Evar_empty;
 		Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar);
-		Evd.evar_candidates = None;
-		Evd.evar_extra = extra }
+                Evd.evar_candidates = None }
     in
-    let evi = Typeclasses.mark_unresolvable evi in
     let (evars, evk) = Evarutil.new_pure_evar_full evars evi in
+    let evars = Evd.set_resolvable_evar evars evk false in
     let evars = Evd.restore_future_goals evars prev_future_goals in
     let ctxt = Environ.named_context_of_val hyps in
     let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in
diff --git a/proofs/goal.mli b/proofs/goal.mli
index a033d6daab..3b31cff8d7 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -39,16 +39,12 @@ module V82 : sig
   (* Access to ".evar_concl" *)
   val concl : Evd.evar_map -> goal -> EConstr.constr
 
-  (* Access to ".evar_extra" *)
-  val extra : Evd.evar_map -> goal -> Evd.Store.t
-
-  (* Old style mk_goal primitive, returns a new goal with corresponding 
+  (* Old style mk_goal primitive, returns a new goal with corresponding
        hypotheses and conclusion, together with a term which is precisely
        the evar corresponding to the goal, and an updated evar_map. *)
   val mk_goal : Evd.evar_map -> 
                          Environ.named_context_val ->
                          EConstr.constr ->
-                         Evd.Store.t ->
                          goal * EConstr.constr * Evd.evar_map
 
   (* Instantiates a goal with an open term *)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 285240872e..254c93d0a2 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -350,7 +350,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
   let env = Goal.V82.env sigma goal in
   let hyps = Goal.V82.hyps sigma goal in
   let mk_goal hyps concl =
-    Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal)
+    Goal.V82.mk_goal sigma hyps concl
   in
     if (not !check) && not (occur_meta sigma (EConstr.of_constr trm)) then
       let t'ty = Retyping.get_type_of env sigma (EConstr.of_constr trm) in
@@ -433,7 +433,7 @@ and mk_hdgoals sigma goal goalacc trm =
   let env = Goal.V82.env sigma goal in
   let hyps = Goal.V82.hyps sigma goal in
   let mk_goal hyps concl = 
-    Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in
+    Goal.V82.mk_goal sigma hyps concl in
   match kind trm with
     | Cast (c,_, ty) when isMeta c ->
 	check_typability env sigma ty;
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 9bd406e14d..f075e5e44a 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -513,12 +513,12 @@ let top_sort evm undefs =
 
 let evars_to_goals p evm =
   let goals = ref Evar.Map.empty in
-  let map ev evi =
-    let evi, goal = p evm ev evi in
+  let fold ev evi evm =
+    let evm, goal = p evm ev evi in
     let () = if goal then goals := Evar.Map.add ev evi !goals in
-    evi
+    evm
   in
-  let evm = Evd.raw_map_undefined map evm in
+  let evm = Evd.fold_undefined fold evm evm in
   if Evar.Map.is_empty !goals then None
   else Some (!goals, evm)
 
@@ -643,10 +643,7 @@ module Search = struct
 
   let mark_unresolvables sigma goals =
     List.fold_left
-      (fun sigma gl ->
-        let evi = Evd.find_undefined sigma gl in
-	let evi' = Typeclasses.mark_unresolvable evi in
-	Evd.add sigma gl evi')
+      (fun sigma gl -> Evd.set_resolvable_evar sigma gl false)
       sigma goals
 
   (** The general hint application tactic.
@@ -1019,7 +1016,7 @@ let deps_of_constraints cstrs evm p =
 let evar_dependencies pred evm p =
   Evd.fold_undefined
     (fun ev evi _ ->
-      if Typeclasses.is_resolvable evi && pred evm ev evi then
+      if Evd.is_resolvable_evar evm ev && pred evm ev evi then
         let evars = Evar.Set.add ev (Evarutil.undefined_evars_of_evar_info evm evi)
         in Intpart.union_set evars p
       else ())
@@ -1036,7 +1033,7 @@ let split_evars pred evm =
 let is_inference_forced p evd ev =
   try
     let evi = Evd.find_undefined evd ev in
-    if Typeclasses.is_resolvable evi && snd (p ev evi)
+    if Evd.is_resolvable_evar evd ev && snd (p ev evi)
     then
       let (loc, k) = evar_source ev evd in
       match k with
@@ -1076,13 +1073,13 @@ let error_unresolvable env comp evd =
 let select_and_update_evars p oevd in_comp evd ev evi =
   assert (evi.evar_body == Evar_empty);
   try
-    let oevi = Evd.find_undefined oevd ev in
-    if Typeclasses.is_resolvable oevi then
-      Typeclasses.mark_unresolvable evi,
+    let _ = Evd.find_undefined oevd ev in
+    if Evd.is_resolvable_evar oevd ev then
+      Evd.set_resolvable_evar evd ev false,
       (in_comp ev && p evd ev evi)
-    else evi, false
+    else evd, false
   with Not_found ->
-    Typeclasses.mark_unresolvable evi, p evd ev evi
+    Evd.set_resolvable_evar evd ev false, p evd ev evi
 
 (** Do we still have unresolved evars that should be resolved ? *)
 
@@ -1095,17 +1092,17 @@ let has_undefined p oevd evd =
     just for this call to resolution. *)
 
 let revert_resolvability oevd evd =
-  let map ev evi =
+  let fold ev _evi evd =
     try
-      if not (Typeclasses.is_resolvable evi) then
-        let evi' = Evd.find_undefined oevd ev in
-        if Typeclasses.is_resolvable evi' then
-          Typeclasses.mark_resolvable evi
-        else evi
-      else evi
-    with Not_found -> evi
+      if not (Evd.is_resolvable_evar evd ev) then
+        let _evi' = Evd.find_undefined oevd ev in
+        if Evd.is_resolvable_evar oevd ev then
+          Evd.set_resolvable_evar evd ev true
+        else evd
+      else evd
+    with Not_found -> evd
   in
-  Evd.raw_map_undefined map evd
+  Evd.fold_undefined fold evd evd
 
 exception Unresolved
 
@@ -1161,8 +1158,7 @@ let _ =
 let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique =
   let (term, sigma) = Hints.wrap_hint_warning_fun env sigma begin fun sigma ->
   let nc, gl, subst, _ = Evarutil.push_rel_context_to_named_context env sigma gl in
-  let (gl,t,sigma) =
-    Goal.V82.mk_goal sigma nc gl Store.empty in
+  let (gl,t,sigma) = Goal.V82.mk_goal sigma nc gl in
   let (ev, _) = destEvar sigma t in
   let gls = { it = gl ; sigma = sigma; } in
   let hints = searchtable_map typeclasses_db in
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index f2bc679aac..6388aa2c33 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -72,11 +72,10 @@ let choose_noteq eqonleft =
 let generalize_right mk typ c1 c2 =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
-    let store = Proofview.Goal.extra gl in
   Refine.refine ~typecheck:false begin fun sigma ->
     let na = Name (next_name_away_with_default "x" Anonymous (Termops.vars_of_env env)) in
     let newconcl = mkProd (na, typ, mk typ c1 (mkRel 1)) in
-    let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store newconcl in
+    let (sigma, x) = Evarutil.new_evar env sigma ~principal:true newconcl in
     (sigma, mkApp (x, [|c2|]))
   end
   end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 18ddc9318d..a6a104ccca 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -117,14 +117,14 @@ let _ =
 
 (** This tactic creates a partial proof realizing the introduction rule, but
     does not check anything. *)
-let unsafe_intro env store decl b =
+let unsafe_intro env decl b =
   Refine.refine ~typecheck:false begin fun sigma ->
     let ctx = named_context_val env in
     let nctx = push_named_context_val decl ctx in
     let inst = List.map (NamedDecl.get_id %> mkVar) (named_context env) in
     let ninst = mkRel 1 :: inst in
     let nb = subst1 (mkVar (NamedDecl.get_id decl)) b in
-    let (sigma, ev) = new_evar_instance nctx sigma nb ~principal:true ~store ninst in
+    let (sigma, ev) = new_evar_instance nctx sigma nb ~principal:true ninst in
     (sigma, mkLambda_or_LetIn (NamedDecl.to_rel_decl decl) ev)
   end
 
@@ -133,7 +133,6 @@ let introduction id =
     let concl = Proofview.Goal.concl gl in
     let sigma = Tacmach.New.project gl in
     let hyps = named_context_val (Proofview.Goal.env gl) in
-    let store = Proofview.Goal.extra gl in
     let env = Proofview.Goal.env gl in
     let () = if mem_named_context_val id hyps then
       user_err ~hdr:"Tactics.introduction"
@@ -141,8 +140,8 @@ let introduction id =
     in
     let open Context.Named.Declaration in
     match EConstr.kind sigma concl with
-    | Prod (_, t, b) -> unsafe_intro env store (LocalAssum (id, t)) b
-    | LetIn (_, c, t, b) -> unsafe_intro env store (LocalDef (id, c, t)) b
+    | Prod (_, t, b) -> unsafe_intro env (LocalAssum (id, t)) b
+    | LetIn (_, c, t, b) -> unsafe_intro env (LocalDef (id, c, t)) b
     | _ -> raise (RefinerError (env, sigma, IntroNeedsProduct))
   end
 
@@ -152,7 +151,6 @@ let error msg = CErrors.user_err Pp.(str msg)
 let convert_concl ?(check=true) ty k =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
-    let store = Proofview.Goal.extra gl in
     let conclty = Proofview.Goal.concl gl in
     Refine.refine ~typecheck:false begin fun sigma ->
       let sigma =
@@ -162,7 +160,7 @@ let convert_concl ?(check=true) ty k =
           | None -> error "Not convertible."
           | Some sigma -> sigma
         end else sigma in
-      let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store ty in
+      let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ty in
       let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in
       (sigma, ans)
     end
@@ -173,11 +171,10 @@ let convert_hyp ?(check=true) d =
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let ty = Proofview.Goal.concl gl in
-    let store = Proofview.Goal.extra gl in
     let sign = convert_hyp check (named_context_val env) sigma d in
     let env = reset_with_named_context sign env in
     Refine.refine ~typecheck:false begin fun sigma ->
-      Evarutil.new_evar env sigma ~principal:true ~store ty
+      Evarutil.new_evar env sigma ~principal:true ty
     end
   end
 
@@ -284,12 +281,11 @@ let move_hyp id dest =
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let ty = Proofview.Goal.concl gl in
-    let store = Proofview.Goal.extra gl in
     let sign = named_context_val env in
     let sign' = move_hyp_in_named_context env sigma id dest sign in
     let env = reset_with_named_context sign' env in
     Refine.refine ~typecheck:false begin fun sigma ->
-      Evarutil.new_evar env sigma ~principal:true ~store ty
+      Evarutil.new_evar env sigma ~principal:true ty
     end
   end
 
@@ -313,7 +309,6 @@ let rename_hyp repl =
     Proofview.Goal.enter begin fun gl ->
       let hyps = Proofview.Goal.hyps gl in
       let concl = Proofview.Goal.concl gl in
-      let store = Proofview.Goal.extra gl in
       let env = Proofview.Goal.env gl in
       let sigma = Proofview.Goal.sigma gl in
       (** Check that we do not mess variables *)
@@ -344,7 +339,7 @@ let rename_hyp repl =
       let nctx = val_of_named_context nhyps in
       let instance = List.map (NamedDecl.get_id %> mkVar) hyps in
       Refine.refine ~typecheck:false begin fun sigma ->
-        Evarutil.new_evar_instance nctx sigma nconcl ~principal:true ~store instance
+        Evarutil.new_evar_instance nctx sigma nconcl ~principal:true instance
       end
     end
 
@@ -445,7 +440,6 @@ let internal_cut_gen ?(check=true) dir replace id t =
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let concl = Proofview.Goal.concl gl in
-    let store = Proofview.Goal.extra gl in
     let sign = named_context_val env in
     let sign',t,concl,sigma =
       if replace then
@@ -464,10 +458,10 @@ let internal_cut_gen ?(check=true) dir replace id t =
         let (sigma,ev,ev') =
           if dir then
             let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in
-            let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true ~store concl in
+            let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true concl in
             (sigma,ev,ev')
           else
-            let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true ~store concl in
+            let (sigma, ev') = Evarutil.new_evar_from_context sign' sigma ~principal:true concl in
             let (sigma, ev) = Evarutil.new_evar_from_context sign sigma nf_t in
             (sigma,ev,ev') in
         let term = mkLetIn (Name id, ev, t, EConstr.Vars.subst_var id ev') in
@@ -2102,11 +2096,10 @@ let keep hyps =
 let apply_type ~typecheck newcl args =
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
-    let store = Proofview.Goal.extra gl in
     Refine.refine ~typecheck begin fun sigma ->
       let newcl = nf_betaiota env sigma newcl (* As in former Logic.refine *) in
       let (sigma, ev) =
-        Evarutil.new_evar env sigma ~principal:true ~store newcl in
+        Evarutil.new_evar env sigma ~principal:true newcl in
       (sigma, applist (ev, args))
     end
   end
@@ -2120,13 +2113,12 @@ let bring_hyps hyps =
   else
     Proofview.Goal.enter begin fun gl ->
       let env = Proofview.Goal.env gl in
-      let store = Proofview.Goal.extra gl in
       let concl = Tacmach.New.pf_concl gl in
       let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
       let args = Array.of_list (Context.Named.to_instance mkVar hyps) in
       Refine.refine ~typecheck:false begin fun sigma ->
         let (sigma, ev) =
-          Evarutil.new_evar env sigma ~principal:true ~store newcl in
+          Evarutil.new_evar env sigma ~principal:true newcl in
         (sigma, mkApp (ev, args))
       end
     end
@@ -2668,7 +2660,7 @@ let mk_eq_name env id {CAst.loc;v=ido} =
 
 (* unsafe *)
 
-let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
+let mkletin_goal env sigma with_eq dep (id,lastlhyp,ccl,c) ty =
   let open Context.Named.Declaration in
   let t = match ty with Some t -> t | _ -> typ_of env sigma c in
   let decl = if dep then LocalDef (id,c,t)
@@ -2683,11 +2675,11 @@ let mkletin_goal env sigma store with_eq dep (id,lastlhyp,ccl,c) ty =
       let eq = applist (eq,args) in
       let refl = applist (refl, [t;mkVar id]) in
       let newenv = insert_before [LocalAssum (heq,eq); decl] lastlhyp env in
-      let (sigma, x) = new_evar newenv sigma ~principal:true ~store ccl in
+      let (sigma, x) = new_evar newenv sigma ~principal:true ccl in
       (sigma, mkNamedLetIn id c t (mkNamedLetIn heq refl eq x))
   | None ->
       let newenv = insert_before [decl] lastlhyp env in
-      let (sigma, x) = new_evar newenv sigma ~principal:true ~store ccl in
+      let (sigma, x) = new_evar newenv sigma ~principal:true ccl in
       (sigma, mkNamedLetIn id c t x)
 
 let pose_tac na c =
@@ -4431,7 +4423,6 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
   let sigma = Proofview.Goal.sigma gl in
   let env = Proofview.Goal.env gl in
   let ccl = Proofview.Goal.concl gl in
-  let store = Proofview.Goal.extra gl in
   let check = check_enough_applied env sigma elim in
   let (sigma', c) = use_bindings env sigma elim false (c0,lbind) t0 in
   let abs = AbstractPattern (from_prefix,check,Name id,(pending,c),cls,false) in
@@ -4457,7 +4448,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
           let b = not with_evars && with_eq != None in
           let (sigma, c) = use_bindings env sigma elim b (c0,lbind) t0 in
           let t = Retyping.get_type_of env sigma c in
-          mkletin_goal env sigma store with_eq false (id,lastlhyp,ccl,c) (Some t)
+          mkletin_goal env sigma with_eq false (id,lastlhyp,ccl,c) (Some t)
         end;
         if with_evars then Proofview.shelve_unifiable else guard_no_unifiable;
         if is_arg_pure_hyp
@@ -4478,7 +4469,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim
       let tac =
       Tacticals.New.tclTHENLIST [
         Refine.refine ~typecheck:false begin fun sigma ->
-          mkletin_goal env sigma store with_eq true (id,lastlhyp,ccl,c) None
+          mkletin_goal env sigma with_eq true (id,lastlhyp,ccl,c) None
         end;
         (tac inhyps)
       ]
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index a4b3a75c9f..50febdf448 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -776,9 +776,9 @@ let explain_unsatisfiable_constraints env sigma constr comp =
   let undef = Evd.undefined_map sigma in
   (** Only keep evars that are subject to resolution and members of the given
      component. *)
-  let is_kept evk evi = match comp with
-  | None -> Typeclasses.is_resolvable evi
-  | Some comp -> Typeclasses.is_resolvable evi && Evar.Set.mem evk comp
+  let is_kept evk _ = match comp with
+  | None -> Evd.is_resolvable_evar sigma evk
+  | Some comp -> Evd.is_resolvable_evar sigma evk && Evar.Set.mem evk comp
   in
   let undef = 
     let m = Evar.Map.filter is_kept undef in