From 9f65b8bf9775dd571a806e10ac356b1b8f8ae2c5 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 8 Oct 2018 02:14:07 +0200
Subject: Cleanup evar_extra: remove evar_info's store and add maps to evar_map

---
 engine/evarutil.ml                 | 19 ++++----
 engine/evarutil.mli                |  8 ++--
 engine/evd.ml                      | 89 ++++++++++++++++++++++++++++++--------
 engine/evd.mli                     | 26 ++++++++---
 engine/proofview.ml                | 24 +++-------
 engine/proofview.mli               |  3 --
 engine/termops.ml                  |  8 +++-
 plugins/ltac/rewrite.ml            |  4 +-
 plugins/setoid_ring/newring.ml     |  2 +-
 plugins/ssr/ssrcommon.ml           |  8 ++--
 plugins/ssrmatching/ssrmatching.ml |  2 +-
 pretyping/evarsolve.ml             | 33 +++++++-------
 pretyping/pretyping.ml             |  9 ++++
 pretyping/typeclasses.ml           | 45 ++++---------------
 pretyping/typeclasses.mli          |  5 +--
 proofs/clenv.ml                    |  4 +-
 proofs/clenvtac.ml                 |  4 +-
 proofs/goal.ml                     | 12 ++---
 proofs/goal.mli                    |  6 +--
 proofs/logic.ml                    |  4 +-
 tactics/class_tactics.ml           | 48 ++++++++++----------
 tactics/eqdecide.ml                |  3 +-
 tactics/tactics.ml                 | 43 ++++++++----------
 vernac/himsg.ml                    |  6 +--
 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
-- 
cgit v1.2.3


From 3e5c6c032dbafda792cef045e83a2cac22256ac3 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 12 Oct 2018 14:54:00 +0200
Subject: PR 8671: Add overlay for plugin-tutorial

---
 dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh | 7 +++++++
 1 file changed, 7 insertions(+)
 create mode 100644 dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh

diff --git a/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh b/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh
new file mode 100644
index 0000000000..fc831574eb
--- /dev/null
+++ b/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh
@@ -0,0 +1,7 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "8671" ] || [ "$CI_BRANCH" = "evar_info-flags" ]; then
+    plugin_tutorial_CI_REF=pr8671-fix
+    plugin_tutorial_CI_GITURL=https://github.com/mattam82/plugin_tutorials
+
+fi
-- 
cgit v1.2.3


From bc238a835ab705d97b37fd74441caaedc639a1f7 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 17 Oct 2018 12:57:18 +0200
Subject: Fix overlay for this extension of the PR. To be removed.

---
 dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh b/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh
index fc831574eb..bd3e1bf7ff 100644
--- a/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh
+++ b/dev/ci/user-overlays/08671-mattam-plugin-tutorials.sh
@@ -1,6 +1,6 @@
 #!/bin/sh
 
-if [ "$CI_PULL_REQUEST" = "8671" ] || [ "$CI_BRANCH" = "evar_info-flags" ]; then
+if [ "$CI_PULL_REQUEST" = "8741" ] || [ "$CI_BRANCH" = "typeclasses-functional-evar_map" ]; then
     plugin_tutorial_CI_REF=pr8671-fix
     plugin_tutorial_CI_GITURL=https://github.com/mattam82/plugin_tutorials
 
-- 
cgit v1.2.3


From fb1c2a017ef8112e061771db14ccc6cc1f09d41c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 16 Oct 2018 12:30:59 +0200
Subject: [typeclasses] functionalize typeclass evar handling

This avoids all the side effects associated with the manipulation of an
unresolvable flag. In the new design:

- The evar_map stores a set of evars that are candidates for typeclass
  resolution, which can be retrieved and set.

  We maintain the invariant that it always contains only undefined
  evars.

- At the creation time of an evar (new_evar), we classify it as a
  potential candidate of resolution.

  - This uses a hook to test if the conclusion ends in a typeclass
    application. (hook set in typeclasses.ml)

  - This is an approximation if the conclusion is an existential (i.e.
    not yet determined). In that case we register the evar as
    potentially a typeclass instance, and later phases must consider
    that case, dropping the evar if it is not a typeclass.

  - One can pass the ~typeclass_candidate:false flag to new_evar to
    prevent classification entirely. Typically this is for new goals
    which should not ever be considered to be typeclass resolution
    candidates.

  - One can mark a subset of evars unresolvable later if
    needed. Typically for clausenv, and marking future goals as
    unresolvable even if they are typeclass goals. For clausenv for
    example, after turing metas into evars we first (optionally) try a
    typeclass resolution on the newly created evars and only then mark
    the remaining newly created evars as subgoals. The intent of the
    code looks clearer now.

  This should prevent keeping testing if undefined evars are classes
  all the time and crawling large sets when no typeclasses are present.

- Typeclass candidate evars stay candidates through
  restriction/evar-evar solutions.

- Evd.add uses ~typeclass_candidate:false to avoid recomputing if the new
  evar is a candidate. There's a deficiency in the API, in most use
  cases of Evd.add we should rather use a:

  `Evd.update_evar_info : evar_map -> Evar.t -> (evar_info -> evar_info)
  -> evar_map`

  Usually it is only about nf_evar'ing the evar_info's contents, which
  doesn't change the evar candidate status.

- Typeclass resolution can now handle the set of candidates
  functionally: it always starts from the set of candidates (and not the
  whole undefined_map) and a filter on it, potentially splitting it in
  connected components, does proof search for each component in an
  evar_map with an empty set of typeclass evars (allowing clean
  reentrancy), then reinstates the potential remaining unsolved
  components and filtered out typeclass evars at the end of
  resolution.

  This means no more marking of resolvability/unresolvability
  everywhere, and hopefully a more efficient implementation in general.

- This is on top of the cleanup of evar_info's currently but can
  be made independent.

[typeclasses] Fix cases.ml: none of the new_evars should be typeclass candidates

Solve bug in inheritance of flags in evar-evar solutions.

Renaming unresolvable to typeclass_candidate (positive) and fix maybe_typeclass_hook
---
 engine/evarutil.ml                 |  22 ++++----
 engine/evarutil.mli                |   6 ++-
 engine/evd.ml                      |  96 ++++++++++++++++++++++-----------
 engine/evd.mli                     |  23 +++++---
 engine/proofview.ml                |  46 ++++++++--------
 engine/proofview.mli               |   6 +--
 engine/termops.ml                  |  10 ++--
 plugins/ltac/rewrite.ml            |  16 +++---
 plugins/ssrmatching/ssrmatching.ml |   2 +
 pretyping/cases.ml                 |   7 ++-
 pretyping/evarsolve.ml             |  25 ++++-----
 pretyping/typeclasses.ml           |  56 +++++++++++---------
 pretyping/typeclasses.mli          |   7 ++-
 proofs/clenv.ml                    |  13 +++--
 proofs/clenv.mli                   |   2 +-
 proofs/clenvtac.ml                 |  27 +++-------
 proofs/goal.ml                     |   3 +-
 proofs/proof.ml                    |   2 +-
 proofs/refine.ml                   |   2 +-
 tactics/autorewrite.ml             |   2 +-
 tactics/class_tactics.ml           | 105 ++++++++++++++-----------------------
 vernac/himsg.ml                    |   5 +-
 22 files changed, 248 insertions(+), 235 deletions(-)

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 69830960a9..4e1636e321 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -405,12 +405,13 @@ let push_rel_context_to_named_context ?hypnaming env sigma typ =
 
 let default_source = Loc.tag @@ Evar_kinds.InternalHole
 
-let new_pure_evar_full evd evi =
-  let (evd, evk) = Evd.new_evar evd evi in
+let new_pure_evar_full evd ?typeclass_candidate evi =
+  let (evd, evk) = Evd.new_evar evd ?typeclass_candidate evi in
   let evd = Evd.declare_future_goal evk evd in
   (evd, evk)
 
-let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?naming ?(principal=false) sign evd typ =
+let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?naming ?typeclass_candidate
+    ?(principal=false) sign evd typ =
   let default_naming = IntroAnonymous in
   let naming = Option.default default_naming naming in
   let name = match naming with
@@ -429,21 +430,22 @@ let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?
     evar_source = src;
     evar_candidates = candidates }
   in
-  let (evd, newevk) = Evd.new_evar evd ?name evi in
+  let typeclass_candidate = if principal then Some false else typeclass_candidate in
+  let (evd, newevk) = Evd.new_evar evd ?name ?typeclass_candidate evi in
   let evd =
     if principal then Evd.declare_principal_goal newevk evd
     else Evd.declare_future_goal newevk evd
   in
   (evd, newevk)
 
-let new_evar_instance ?src ?filter ?candidates ?naming ?principal sign evd typ instance =
+let new_evar_instance ?src ?filter ?candidates ?naming ?typeclass_candidate ?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 ?naming ?principal typ in
+  let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal typ in
   evd, mkEvar (newevk,Array.of_list instance)
 
-let new_evar_from_context ?src ?filter ?candidates ?naming ?principal sign evd typ =
+let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ =
   let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in
   let instance =
     match filter with
@@ -453,7 +455,7 @@ let new_evar_from_context ?src ?filter ?candidates ?naming ?principal sign evd t
 
 (* [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 ?naming ?principal ?hypnaming env evd typ =
+let new_evar ?src ?filter ?candidates ?naming ?typeclass_candidate ?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
@@ -461,11 +463,11 @@ let new_evar ?src ?filter ?candidates ?naming ?principal ?hypnaming env evd typ
     match filter with
     | None -> instance
     | Some filter -> Filter.filter_list filter instance in
-  new_evar_instance sign evd typ' ?src ?filter ?candidates ?naming ?principal instance
+  new_evar_instance sign evd typ' ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal instance
 
 let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid =
   let (evd', s) = new_sort_variable rigid evd in
-  let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal ?hypnaming (EConstr.mkSort s) in
+  let (evd', e) = new_evar env evd' ?src ?filter ?naming ~typeclass_candidate:false ?principal ?hypnaming (EConstr.mkSort s) in
   evd', (e, s)
 
 let new_Type ?(rigid=Evd.univ_flexible) evd =
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 49443164cc..0c8d8c9b8a 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -29,6 +29,7 @@ val new_evar_from_context :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?candidates:constr list ->
   ?naming:intro_pattern_naming_expr ->
+  ?typeclass_candidate:bool ->
   ?principal:bool ->
   named_context_val -> evar_map  -> types -> evar_map * EConstr.t
 
@@ -42,6 +43,7 @@ val new_evar :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?candidates:constr list ->
   ?naming:intro_pattern_naming_expr ->
+  ?typeclass_candidate:bool ->
   ?principal:bool -> ?hypnaming:naming_mode ->
   env -> evar_map -> types -> evar_map * EConstr.t
 
@@ -49,10 +51,11 @@ val new_pure_evar :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
   ?candidates:constr list ->
   ?naming:intro_pattern_naming_expr ->
+  ?typeclass_candidate:bool ->
   ?principal:bool ->
   named_context_val -> evar_map -> types -> evar_map * Evar.t
 
-val new_pure_evar_full : evar_map -> evar_info -> evar_map * Evar.t
+val new_pure_evar_full : evar_map -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t
 
 (** Create a new Type existential variable, as we keep track of 
     them during type-checking and unification. *)
@@ -78,6 +81,7 @@ val new_global : evar_map -> GlobRef.t -> evar_map * constr
 val new_evar_instance :
   ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list ->
   ?naming:intro_pattern_naming_expr ->
+  ?typeclass_candidate:bool ->
   ?principal:bool ->
  named_context_val -> evar_map -> types ->
   constr list -> evar_map * constr
diff --git a/engine/evd.ml b/engine/evd.ml
index 3a01706063..3a77a2b440 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -413,7 +413,7 @@ 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 }
+    typeclass_evars : Evar.Set.t }
 
 type evar_map = {
   (** Existential variables *)
@@ -444,44 +444,44 @@ type evar_map = {
   extras : Store.t;
 }
 
+let get_is_maybe_typeclass, (is_maybe_typeclass_hook : (evar_map -> constr -> bool) Hook.t) = Hook.make ~default:(fun evd c -> false) ()
+
+let is_maybe_typeclass sigma c = Hook.get get_is_maybe_typeclass sigma c
+
 (*** Lifting primitive from Evar.Map. ***)
 
 let rename evk id evd =
   { evd with evar_names = EvNames.rename evk id evd.evar_names }
 
-let add_with_name ?name d e i = match i.evar_body with
+let add_with_name ?name ?(typeclass_candidate = true) d e i = match i.evar_body with
 | Evar_empty ->
   let evar_names = EvNames.add_name_undefined name e i d.evar_names in
-  { d with undf_evars = EvMap.add e i d.undf_evars; evar_names }
+  let evar_flags =
+    if typeclass_candidate && is_maybe_typeclass d i.evar_concl then
+      let flags = d.evar_flags in
+      { flags with typeclass_evars = Evar.Set.add e flags.typeclass_evars }
+    else d.evar_flags
+  in
+  { d with undf_evars = EvMap.add e i d.undf_evars; evar_names; evar_flags }
 | Evar_defined _ ->
   let evar_names = EvNames.remove_name_defined e d.evar_names in
   { d with defn_evars = EvMap.add e i d.defn_evars; evar_names }
 
-let add d e i = add_with_name d e i
+(** Evd.add is a low-level function mainly used to update the evar_info
+    associated to an evar, so we prevent registering its typeclass status. *)
+let add d e i = add_with_name ~typeclass_candidate:false d e i
 
-(*** Evar flags: resolvable, restricted or obligation flag *)
+(*** Evar flags: typeclasses, 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 get_typeclass_evars evd = evd.evar_flags.typeclass_evars
 
-let is_resolvable_evar evd evk =
+let set_typeclass_evars evd tcs =
   let flags = evd.evar_flags in
-  not (Evar.Set.mem evk flags.unresolvable_evars)
+  { evd with evar_flags = { flags with typeclass_evars = tcs } }
 
-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 is_typeclass_evar evd evk =
+  let flags = evd.evar_flags in
+  Evar.Set.mem evk flags.typeclass_evars
 
 let set_obligation_evar evd evk =
   let flags = evd.evar_flags in
@@ -492,8 +492,31 @@ let is_obligation_evar evd evk =
   let flags = evd.evar_flags in
   Evar.Set.mem evk flags.obligation_evars
 
+(** Inheritance of flags: for evar-evar and restriction cases *)
+
+let inherit_evar_flags evar_flags evk evk' =
+  let evk_typeclass = Evar.Set.mem evk evar_flags.typeclass_evars in
+  let evk_obligation = Evar.Set.mem evk evar_flags.obligation_evars in
+  if not (evk_obligation || evk_typeclass) then evar_flags
+  else
+    let typeclass_evars =
+      if evk_typeclass then
+        let typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars in
+        Evar.Set.add evk' typeclass_evars
+      else evar_flags.typeclass_evars
+    in
+    let obligation_evars =
+      if evk_obligation then
+        let obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars in
+        Evar.Set.add evk' obligation_evars
+      else evar_flags.obligation_evars
+    in
+    { evar_flags with obligation_evars; typeclass_evars }
+
+(** Removal: in all other cases of definition *)
+
 let remove_evar_flags evk evar_flags =
-  { unresolvable_evars = Evar.Set.remove evk evar_flags.unresolvable_evars;
+  { typeclass_evars = Evar.Set.remove evk evar_flags.typeclass_evars;
     obligation_evars = Evar.Set.remove evk evar_flags.obligation_evars;
     (** Restriction information is kept. *)
     restricted_evars = evar_flags.restricted_evars }
@@ -506,9 +529,9 @@ let evar_counter_summary_name = "evar counter"
 let evar_ctr, evar_counter_summary_tag = Summary.ref_tag 0 ~name:evar_counter_summary_name
 let new_untyped_evar () = incr evar_ctr; Evar.unsafe_of_int !evar_ctr
 
-let new_evar evd ?name evi =
+let new_evar evd ?name ?typeclass_candidate evi =
   let evk = new_untyped_evar () in
-  let evd = add_with_name evd ?name evk evi in
+  let evd = add_with_name evd ?name ?typeclass_candidate evk evi in
   (evd, evk)
 
 let remove d e =
@@ -630,7 +653,7 @@ let create_evar_defs sigma = { sigma with
 let empty_evar_flags =
   { obligation_evars = Evar.Set.empty;
     restricted_evars = Evar.Map.empty;
-    unresolvable_evars = Evar.Set.empty }
+    typeclass_evars = Evar.Set.empty }
 
 let empty = {
   defn_evars = EvMap.empty;
@@ -698,16 +721,26 @@ let define_aux def undef evk body =
   EvMap.add evk newinfo def, EvMap.remove evk undef
 
 (* define the existential of section path sp as the constr body *)
-let define evk body evd =
+let define_gen evk body evd evar_flags =
   let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
   let last_mods = match evd.conv_pbs with
   | [] ->  evd.last_mods
   | _ -> Evar.Set.add evk evd.last_mods
   in
   let evar_names = EvNames.remove_name_defined evk evd.evar_names in
-  let evar_flags = remove_evar_flags evk evd.evar_flags in
   { evd with defn_evars; undf_evars; last_mods; evar_names; evar_flags }
 
+(** By default, the obligation and evar tag of the evar is removed *)
+let define evk body evd =
+  let evar_flags = remove_evar_flags evk evd.evar_flags in
+  define_gen evk body evd evar_flags
+
+(** In case of an evar-evar solution, the flags are inherited *)
+let define_with_evar evk body evd =
+  let evk' = fst (destEvar body) in
+  let evar_flags = inherit_evar_flags evd.evar_flags evk evk' in
+  define_gen evk body evd evar_flags
+
 let is_restricted_evar evd evk =
   try Some (Evar.Map.find evk evd.evar_flags.restricted_evars)
   with Not_found -> None
@@ -715,6 +748,9 @@ let is_restricted_evar evd evk =
 let declare_restricted_evar evar_flags evk evk' =
   { evar_flags with restricted_evars = Evar.Map.add evk evk' evar_flags.restricted_evars }
 
+(* In case of restriction, we declare the restriction and inherit the obligation
+   and typeclass flags. *)
+
 let restrict evk filter ?candidates ?src evd =
   let evk' = new_untyped_evar () in
   let evar_info = EvMap.find evk evd.undf_evars in
@@ -731,7 +767,7 @@ let restrict evk filter ?candidates ?src evd =
   let body = mkEvar(evk',id_inst) 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
+  let evar_flags = inherit_evar_flags evar_flags evk evk' in
   { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
     defn_evars; last_mods; evar_names; evar_flags }, evk'
 
diff --git a/engine/evd.mli b/engine/evd.mli
index 87f74f660d..b0e3c2b869 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -139,7 +139,7 @@ val has_undefined : evar_map -> bool
     there are uninstantiated evars in [sigma]. *)
 
 val new_evar : evar_map ->
-  ?name:Id.t -> evar_info -> evar_map * Evar.t
+  ?name:Id.t -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t
 (** Creates a fresh evar mapping to the given information. *)
 
 val add : evar_map -> Evar.t -> evar_info -> evar_map
@@ -176,7 +176,7 @@ val raw_map_undefined : (Evar.t -> evar_info -> evar_info) -> evar_map -> evar_m
 (** Same as {!raw_map}, but restricted to undefined evars. For efficiency
     reasons. *)
 
-val define : Evar.t-> econstr -> evar_map -> evar_map
+val define : Evar.t -> econstr -> evar_map -> evar_map
 (** Set the body of an evar to the given constr. It is expected that:
     {ul
       {- The evar is already present in the evarmap.}
@@ -184,6 +184,10 @@ val define : Evar.t-> econstr -> evar_map -> evar_map
       {- All the evars present in the constr should be present in the evar map.}
     } *)
 
+val define_with_evar : Evar.t -> econstr -> evar_map -> evar_map
+(** Same as [define ev body evd], except the body must be an existential variable [ev'].
+    This additionally makes [ev'] inherit the [obligation] and [typeclass] flags of [ev]. *)
+
 val cmap : (econstr -> econstr) -> evar_map -> evar_map
 (** Map the function on all terms in the evar map. *)
 
@@ -204,6 +208,8 @@ val undefined_map : evar_map -> evar_info Evar.Map.t
 
 val drop_all_defined : evar_map -> evar_map
 
+val is_maybe_typeclass_hook : (evar_map -> constr -> bool) Hook.t
+
 (** {6 Instantiating partial terms} *)
 
 exception NotInstantiatedEvar
@@ -244,13 +250,16 @@ val restrict : Evar.t-> Filter.t -> ?candidates:econstr list ->
 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 set_typeclass_evars : evar_map -> Evar.Set.t -> evar_map
+(** Mark the given set of evars as available for resolution.
+
+    Precondition: they should indeed refer to undefined typeclass evars.
+ *)
 
-val unresolvable_evars : evar_map -> Evar.Set.t
-(** The set of unresolvable evars *)
+val get_typeclass_evars : evar_map -> Evar.Set.t
+(** The set of undefined typeclass evars *)
 
-val is_resolvable_evar : evar_map -> Evar.t -> bool
+val is_typeclass_evar : evar_map -> Evar.t -> bool
 (** Is the evar declared resolvable for typeclass resolution *)
 
 val set_obligation_evar : evar_map -> Evar.t -> evar_map
diff --git a/engine/proofview.ml b/engine/proofview.ml
index aabc629ee4..304b2dff84 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -67,11 +67,8 @@ let dependent_init =
   let rec aux = function
   | TNil sigma -> [], { solution = sigma; comb = []; shelf = [] }
   | TCons (env, sigma, typ, t) ->
-    let (sigma, econstr) = Evarutil.new_evar env sigma ~src typ in
+    let (sigma, econstr) = Evarutil.new_evar env sigma ~src ~typeclass_candidate:false 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 = [] }
@@ -743,23 +740,28 @@ let unshelve l p =
   let l = undefined p.solution l in
   { p with comb = p.comb@l }
 
-let mark_in_evm ~goal evd content =
-  let info = Evd.find evd content in
-  let info =
+let mark_in_evm ~goal evd evars =
+  let evd =
     if goal then
-      { info with Evd.evar_source = match info.Evd.evar_source with
-            (* Two kinds for goal evars:
-               - GoalEvar (morally not dependent)
-               - VarInstance (morally dependent of some name).
-               This is a heuristic for naming these evars. *)
-  | loc, (Evar_kinds.QuestionMark { Evar_kinds.qm_name=Names.Name id} |
-                    Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id
-            | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
-            | loc,_ -> loc,Evar_kinds.GoalEvar }
-    else info
+      let mark evd content =
+        let info = Evd.find evd content in
+        let info =
+          { info with Evd.evar_source = match info.Evd.evar_source with
+                (* Two kinds for goal evars:
+                   - GoalEvar (morally not dependent)
+                   - VarInstance (morally dependent of some name).
+                   This is a heuristic for naming these evars. *)
+                | loc, (Evar_kinds.QuestionMark { Evar_kinds.qm_name=Names.Name id} |
+                        Evar_kinds.ImplicitArg (_,(_,Some id),_)) -> loc, Evar_kinds.VarInstance id
+                | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
+                | loc,_ -> loc,Evar_kinds.GoalEvar }
+        in Evd.add evd content info
+      in CList.fold_left mark evd evars
+    else evd
   in
-  let evd = Evd.add evd content info in
-  Evd.set_resolvable_evar evd content false
+  let tcs = Evd.get_typeclass_evars evd in
+  let evset = Evar.Set.of_list evars in
+  Evd.set_typeclass_evars evd (Evar.Set.diff tcs evset)
 
 let with_shelf tac =
   let open Proof in
@@ -776,7 +778,7 @@ let with_shelf tac =
   let sigma = Evd.restore_future_goals sigma fgoals in
   (* Ensure we mark and return only unsolved goals *)
   let gls' = undefined_evars sigma (CList.rev_append gls' gls) in
-  let sigma = CList.fold_left (mark_in_evm ~goal:false) sigma gls' in
+  let sigma = mark_in_evm ~goal:false sigma gls' in
   let npv = { npv with shelf; solution = sigma } in
   Pv.set npv >> tclUNIT (gls', ans)
 
@@ -1030,7 +1032,7 @@ module Unsafe = struct
   let reset_future_goals p =
     { p with solution = Evd.reset_future_goals p.solution }
 
-  let mark_as_goal evd content =
+  let mark_as_goals evd content =
     mark_in_evm ~goal:true evd content
 
   let advance = Evarutil.advance
@@ -1038,7 +1040,7 @@ module Unsafe = struct
   let undefined = undefined
 
   let mark_as_unresolvable p gl =
-    { p with solution = mark_in_evm ~goal:false p.solution gl }
+    { p with solution = mark_in_evm ~goal:false p.solution [gl] }
 
 end
 
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 7bf6390f0e..cda4808a23 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -456,9 +456,9 @@ module Unsafe : sig
   (** Clears the future goals store in the proof view. *)
   val reset_future_goals : proofview -> proofview
 
-  (** Give an evar the status of a goal (changes its source location
-      and makes it unresolvable for type classes. *)
-  val mark_as_goal : Evd.evar_map -> Evar.t -> Evd.evar_map
+  (** Give the evars the status of a goal (changes their source location
+      and makes them unresolvable for type classes. *)
+  val mark_as_goals : Evd.evar_map -> Evar.t list -> Evd.evar_map
 
   (** Make an evar unresolvable for type classes. *)
   val mark_as_unresolvable : proofview -> Evar.t -> proofview
diff --git a/engine/termops.ml b/engine/termops.ml
index c4b57e4dd2..5e220fd8f1 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -365,18 +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
+  and typeclasses =
+    let evars = Evd.get_typeclass_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 ()
+      str "TYPECLASSES:" ++ brk (0, 1) ++
+      prlist_with_sep spc Evar.print (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 ++ unresolvables ++ metas
+  evs ++ svs ++ cstrs ++ typeclasses ++ metas
 
 let pr_evar_list sigma l =
   let open Evd in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 8cecf9bd9b..9f7669f1d5 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 (evd', t) = Evarutil.new_evar env evd t in
+  (** We handle the typeclass resolution of constraints ourselves *)
+  let (evd', t) = Evarutil.new_evar env evd ~typeclass_candidate:false 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. *)
@@ -632,9 +632,6 @@ let solve_remaining_by env sigma holes by =
 let no_constraints cstrs = 
   fun ev _ -> not (Evar.Set.mem ev cstrs)
 
-let all_constraints cstrs = 
-  fun ev _ -> Evar.Set.mem ev cstrs
-
 let poly_inverse sort =
   if sort then PropGlobal.inverse else TypeGlobal.inverse
 
@@ -1453,10 +1450,11 @@ let apply_strategy (s : strategy) env unfresh concl (prop, cstr) evars =
   res
 
 let solve_constraints env (evars,cstrs) =
-  let filter = all_constraints cstrs in
-    Typeclasses.resolve_typeclasses env ~filter ~split:false ~fail:true 
-      (Typeclasses.mark_resolvables ~filter evars)
-      
+  let oldtcs = Evd.get_typeclass_evars evars in
+  let evars' = Evd.set_typeclass_evars evars cstrs in
+  let evars' = Typeclasses.resolve_typeclasses env ~filter:all_evars ~split:false ~fail:true evars' in
+  Evd.set_typeclass_evars evars' oldtcs
+
 let nf_zeta =
   Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
 
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index ebba6223b7..7f67487f5d 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -356,8 +356,10 @@ let nf_open_term sigma0 ise c =
 
 let unif_end env sigma0 ise0 pt ok =
   let ise = Evarconv.solve_unif_constraints_with_heuristics env ise0 in
+  let tcs = Evd.get_typeclass_evars ise in
   let s, uc, t = nf_open_term sigma0 ise pt in
   let ise1 = create_evar_defs s in
+  let ise1 = Evd.set_typeclass_evars ise1 (Evar.Set.filter (fun ev -> Evd.is_undefined ise1 ev) tcs) in
   let ise1 = Evd.set_universe_context ise1 uc in
   let ise2 = Typeclasses.resolve_typeclasses ~fail:true env ise1 in
   if not (ok ise) then raise NoProgress else
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 54e847988b..164f5ab96d 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -296,8 +296,7 @@ let inductive_template env sigma tmloc ind =
             let ty = EConstr.of_constr ty in
 	    let ty' = substl subst ty in
             let sigma, e =
-                Evarutil.new_evar env ~src:(hole_source n)
-                sigma ty'
+              Evarutil.new_evar env ~src:(hole_source n) ~typeclass_candidate:false sigma ty'
             in
             (sigma, e::subst,e::evarl,n+1)
 	| LocalDef (na,b,ty) ->
@@ -1698,7 +1697,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t =
 	    (fun i _ ->
               try list_assoc_in_triple i subst0 with Not_found -> mkRel i)
               1 (rel_context !!env) in
-        let sigma, ev' = Evarutil.new_evar ~src !!env sigma ty in
+        let sigma, ev' = Evarutil.new_evar ~src ~typeclass_candidate:false !!env sigma ty in
         begin match solve_simple_eqn (evar_conv_x full_transparent_state) !!env sigma (None,ev,substl inst ev') with
         | Success evd -> evdref := evd
         | UnifFailure _ -> assert false
@@ -1734,7 +1733,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t =
           (named_context !!extenv) in
       let filter = Filter.make (rel_filter @ named_filter) in
       let candidates = List.rev (u :: List.map mkRel vl) in
-      let sigma, ev = Evarutil.new_evar !!extenv ~src ~filter ~candidates sigma ty in
+      let sigma, ev = Evarutil.new_evar !!extenv ~src ~filter ~candidates ~typeclass_candidate:false sigma ty in
       let () = evdref := sigma in
       lift k ev
   in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 9422a96f21..674f6846ae 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1239,26 +1239,21 @@ let check_evar_instance evd evk1 body conv_algo =
   | UnifFailure _ -> raise (IllTypedInstance (evenv,ty, evi.evar_concl))
 
 let update_evar_info ev1 ev2 evd =
+  (* We update the source of obligation evars during evar-evar unifications. *)
   let loc, evs2 = evar_source ev2 evd in
-  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 evi = Evd.find evd ev1 in
+  Evd.add evd ev1 {evi with evar_source = loc, evs2}
 
 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_info (fst (destEvar evd body)) evk2 evd' in
-      check_evar_instance evd' evk2 body g
+    let evd' = Evd.define_with_evar evk2 body evd in
+    let evd' =
+      if is_obligation_evar evd evk2 then
+        update_evar_info evk2 (fst (destEvar evd' body)) evd'
+      else evd'
+    in
+    check_evar_instance evd' evk2 body g
   with EvarSolvedOnTheFly (evd,c) ->
     f env evd pbty ev2 c
 
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 07821f03e5..4aea2c3db9 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -166,6 +166,21 @@ let rec is_class_type evd c =
 let is_class_evar evd evi =
   is_class_type evd evi.Evd.evar_concl
 
+let is_class_constr sigma c =
+  try let gr, u = Termops.global_of_constr sigma c in
+    GlobRef.Map.mem gr !classes
+  with Not_found -> false
+
+let rec is_maybe_class_type evd c =
+  let c, _ = Termops.decompose_app_vect evd c in
+    match EConstr.kind evd c with
+    | Prod (_, _, t) -> is_maybe_class_type evd t
+    | Cast (t, _, _) -> is_maybe_class_type evd t
+    | Evar _ -> true
+    | _ -> is_class_constr evd c
+
+let () = Hook.set Evd.is_maybe_typeclass_hook (fun evd c -> is_maybe_class_type evd (EConstr.of_constr c))
+
 (*
  * classes persistent object
  *)
@@ -481,36 +496,29 @@ let instances r =
 let is_class gr = 
   GlobRef.Map.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes
 
-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
+type evar_filter = Evar.t -> Evar_kinds.t Lazy.t -> bool
+
+let make_unresolvables filter evd =
+  let tcs = Evd.get_typeclass_evars evd in
+  Evd.set_typeclass_evars evd (Evar.Set.filter (fun x -> not (filter x)) tcs)
 
 let all_evars _ _ = true
-let all_goals _ = function VarInstance _ | GoalEvar -> true | _ -> false
+let all_goals _ source =
+  match Lazy.force source with
+  | VarInstance _ | GoalEvar -> true
+  | _ -> false
+
 let no_goals ev evi = not (all_goals ev evi)
-let no_goals_or_obligations _ = function
+let no_goals_or_obligations _ source =
+  match Lazy.force source with
   | VarInstance _ | GoalEvar | QuestionMark _ -> false
   | _ -> true
 
-let mark_resolvability filter b sigma =
-  let map ev evi evm =
-    if filter ev (snd evi.evar_source) then mark_resolvability_undef evm ev b
-    else evm
-  in
-  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) && Evd.is_resolvable_evar evd ev && is_class_evar evd evi
-  in
-  Evar.Map.exists check (Evd.undefined_map evd)
+  let tcs = get_typeclass_evars evd in
+  let check ev = filter ev (lazy (snd (Evd.find evd ev).evar_source)) in
+  Evar.Set.exists check tcs
 
 let get_solve_all_instances, solve_all_instances_hook = Hook.make ()
 
@@ -521,7 +529,7 @@ let solve_all_instances env evd filter unique split fail =
 (* let solve_classeskey = CProfile.declare_profile "solve_typeclasses" *)
 (* let solve_problem = CProfile.profile5 solve_classeskey solve_problem *)
 
-let resolve_typeclasses ?(fast_path = true) ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ())
+let resolve_typeclasses ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ())
     ?(split=true) ?(fail=true) env evd =
-  if fast_path && not (has_typeclasses filter evd) then evd
+  if not (has_typeclasses filter evd) then evd
   else solve_all_instances env evd filter unique split fail
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index de9a99a868..ee9c83dad3 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -93,7 +93,7 @@ val instance_constructor : typeclass EConstr.puniverses -> EConstr.t list ->
   EConstr.t option * EConstr.t
 
 (** Filter which evars to consider for resolution. *)
-type evar_filter = Evar.t -> Evar_kinds.t -> bool
+type evar_filter = Evar.t -> Evar_kinds.t Lazy.t -> bool
 val all_evars : evar_filter
 val all_goals : evar_filter
 val no_goals : evar_filter
@@ -107,13 +107,12 @@ val no_goals_or_obligations : evar_filter
     An unresolvable evar is an evar the type-class engine will NOT try to solve
 *)
 
-val mark_unresolvables : ?filter:evar_filter -> evar_map -> evar_map
-val mark_resolvables   : ?filter:evar_filter -> evar_map -> evar_map
+val make_unresolvables : (Evar.t -> bool) -> evar_map -> evar_map
 
 val is_class_evar : evar_map -> evar_info -> bool
 val is_class_type : evar_map -> EConstr.types -> bool
 
-val resolve_typeclasses : ?fast_path:bool -> ?filter:evar_filter -> ?unique:bool ->
+val resolve_typeclasses : ?filter:evar_filter -> ?unique:bool ->
   ?split:bool -> ?fail:bool -> env -> evar_map -> evar_map
 val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> EConstr.types -> evar_map * EConstr.constr
 
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 7ebc789aa5..d25ae38c53 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -324,21 +324,21 @@ let adjust_meta_source evd mv = function
 *)
 
 let clenv_pose_metas_as_evars clenv dep_mvs =
-  let rec fold clenv = function
-  | [] -> clenv
+  let rec fold clenv evs = function
+  | [] -> clenv, evs
   | mv::mvs ->
       let ty = clenv_meta_type clenv mv in
       (* Postpone the evar-ization if dependent on another meta *)
       (* This assumes no cycle in the dependencies - is it correct ? *)
-      if occur_meta clenv.evd ty then fold clenv (mvs@[mv])
+      if occur_meta clenv.evd ty then fold clenv evs (mvs@[mv])
       else
         let src = evar_source_of_meta mv clenv.evd in
         let src = adjust_meta_source clenv.evd mv src in
         let evd = clenv.evd in
 	let (evd, evar) = new_evar (cl_env clenv) evd ~src ty in
 	let clenv = clenv_assign mv evar {clenv with evd=evd} in
-	fold clenv mvs in
-  fold clenv dep_mvs
+        fold clenv (fst (destEvar evd evar) :: evs) mvs in
+  fold clenv [] dep_mvs
 
 (******************************************************************)
 
@@ -608,8 +608,7 @@ 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 (sigma, ev) = new_evar env sigma t1 in
-      let sigma = Evd.set_resolvable_evar sigma (fst (destEvar sigma ev)) false in
+      let (sigma, ev) = new_evar env sigma ~typeclass_candidate:false t1 in
       let dep = not (noccurn sigma 1 t2) in
       let hole = {
         hole_evar = ev;
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index f9506290a0..03acb9e46e 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -72,7 +72,7 @@ val clenv_unique_resolver :
 
 val clenv_dependent : clausenv -> metavariable list
 
-val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
+val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv * Evar.t list
 
 (** {6 Bindings } *)
 
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 929443a969..77f5804665 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -62,37 +62,19 @@ let clenv_pose_dependent_evars ?(with_evars=false) clenv =
       (RefinerError (env, sigma, UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
   clenv_pose_metas_as_evars clenv dep_mvs
 
-(** Use our own fast path, more informative than from Typeclasses *)
-let check_tc evd =
-  let has_resolvable = ref false 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
-    else false
-  in
-  let has_typeclass = Evar.Map.exists check (Evd.undefined_map evd) in
-  (has_typeclass, !has_resolvable)
-
 let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
   (** ppedrot: a Goal.enter here breaks things, because the tactic below may
       solve goals by side effects, while the compatibility layer keeps those
       useless goals. That deserves a FIXME. *)
   Proofview.V82.tactic begin fun gl ->
-  let clenv = clenv_pose_dependent_evars ~with_evars clenv in
+  let clenv, evars = clenv_pose_dependent_evars ~with_evars clenv in
   let evd' =
     if with_classes then
-      let (has_typeclass, has_resolvable) = check_tc clenv.evd in
       let evd' =
-        if has_typeclass then
-          Typeclasses.resolve_typeclasses ~fast_path:false ~filter:Typeclasses.all_evars
+        Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
           ~fail:(not with_evars) ~split:false clenv.env clenv.evd
-        else clenv.evd
       in
-      if has_resolvable then
-        Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals evd'
-      else evd'
+      Typeclasses.make_unresolvables (fun x -> List.mem_f Evar.equal x evars) evd'
     else clenv.evd
   in
   let clenv = { clenv with evd = evd' } in
@@ -101,6 +83,9 @@ let clenv_refine ?(with_evars=false) ?(with_classes=true) clenv =
     (refine_no_check (clenv_cast_meta clenv (clenv_value clenv))) gl
   end
 
+let clenv_pose_dependent_evars ?(with_evars=false) clenv =
+  fst (clenv_pose_dependent_evars ~with_evars clenv)
+
 open Unification
 
 let dft = default_unify_flags
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 6aff43f741..4e540de538 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -64,8 +64,7 @@ module V82 = struct
 		Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar);
                 Evd.evar_candidates = None }
     in
-    let (evars, evk) = Evarutil.new_pure_evar_full evars evi in
-    let evars = Evd.set_resolvable_evar evars evk false in
+    let (evars, evk) = Evarutil.new_pure_evar_full evars ~typeclass_candidate:false evi 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/proof.ml b/proofs/proof.ml
index 70a08e4966..8220949856 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -386,7 +386,7 @@ let run_tactic env tac pr =
     (* Check that retrieved given up is empty *)
     if not (List.is_empty retrieved_given_up) then
       CErrors.anomaly Pp.(str "Evars generated outside of proof engine (e.g. V82, clear, ...) are not supposed to be explicitly given up.");
-    let sigma = List.fold_left Proofview.Unsafe.mark_as_goal sigma retrieved in
+    let sigma = Proofview.Unsafe.mark_as_goals sigma retrieved in
     Proofview.Unsafe.tclEVARS sigma >>= fun () ->
     Proofview.tclUNIT retrieved
   in
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 05474d5f84..540a8bb420 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -105,7 +105,7 @@ let generic_refine ~typecheck f gl =
         | Some id -> Evd.rename evk id sigma
   in
   (** Mark goals *)
-  let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in
+  let sigma = Proofview.Unsafe.mark_as_goals sigma comb in
   let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in
   let trace () = Pp.(hov 2 (str"simple refine"++spc()++
                             Termops.Internal.print_constr_env env sigma c)) in
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 8e296de617..76cbdee0d5 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -226,7 +226,7 @@ let decompose_applied_relation metas env sigma c ctype left2right =
     let eqclause = Clenv.mk_clenv_from_env env sigma None (EConstr.of_constr c,ty) in
     let eqclause =
       if metas then eqclause
-      else clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd)
+      else fst (clenv_pose_metas_as_evars eqclause (Evd.undefined_metas eqclause.evd))
     in
     let (equiv, args) = EConstr.decompose_app sigma (Clenv.clenv_type eqclause) in
     let rec split_last_two = function
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index f075e5e44a..81cf9289d1 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -494,15 +494,15 @@ let top_sort evm undefs =
   let tosee = ref undefs in
   let rec visit ev evi =
     let evs = Evarutil.undefined_evars_of_evar_info evm evi in
-      tosee := Evar.Map.remove ev !tosee;
+      tosee := Evar.Set.remove ev !tosee;
       Evar.Set.iter (fun ev ->
-        if Evar.Map.mem ev !tosee then
-          visit ev (Evar.Map.find ev !tosee)) evs;
+        if Evar.Set.mem ev !tosee then
+          visit ev (Evd.find evm ev)) evs;
       l' := ev :: !l';
   in
-    while not (Evar.Map.is_empty !tosee) do
-      let ev, evi = Evar.Map.min_binding !tosee in
-        visit ev evi
+    while not (Evar.Set.is_empty !tosee) do
+      let ev = Evar.Set.choose !tosee in
+        visit ev (Evd.find evm ev)
     done;
     List.rev !l'
 
@@ -512,15 +512,9 @@ let top_sort evm undefs =
 *)
 
 let evars_to_goals p evm =
-  let goals = ref Evar.Map.empty 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
-    evm
-  in
-  let evm = Evd.fold_undefined fold evm evm in
-  if Evar.Map.is_empty !goals then None
-  else Some (!goals, evm)
+  let goals, nongoals = Evar.Set.partition (p evm) (Evd.get_typeclass_evars evm) in
+  if Evar.Set.is_empty goals then None
+  else Some (goals, nongoals)
 
 (** Making local hints  *)
 let make_resolve_hyp env sigma st flags only_classes pri decl =
@@ -641,11 +635,6 @@ module Search = struct
       occur_existential evd concl
     else true
 
-  let mark_unresolvables sigma goals =
-    List.fold_left
-      (fun sigma gl -> Evd.set_resolvable_evar sigma gl false)
-      sigma goals
-
   (** The general hint application tactic.
       tac1 + tac2 .... The choice of OR or ORELSE is determined
       depending on the dependencies of the goal and the unique/Prop
@@ -776,7 +765,7 @@ module Search = struct
             shelve_goals shelved <*>
               (if List.is_empty goals then tclUNIT ()
                else
-	         let sigma' = mark_unresolvables sigma goals in
+                 let sigma' = make_unresolvables (fun x -> List.mem_f Evar.equal x goals) sigma in
                  with_shelf (Unsafe.tclEVARS sigma' <*> Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state goals)) >>=
                       fun s -> result s i (Some (Option.default 0 k + j)))
           end
@@ -938,14 +927,15 @@ module Search = struct
   let run_on_evars env evm p tac =
     match evars_to_goals p evm with
     | None -> None (* This happens only because there's no evar having p *)
-    | Some (goals, evm') ->
+    | Some (goals, nongoals) ->
        let goals =
          if !typeclasses_dependency_order then
-           top_sort evm' goals
-         else List.map (fun (ev, _) -> ev) (Evar.Map.bindings goals)
+           top_sort evm goals
+         else Evar.Set.elements goals
        in
+       let evm = Evd.set_typeclass_evars evm Evar.Set.empty in
        let fgoals = Evd.save_future_goals evm in
-       let _, pv = Proofview.init evm' [] in
+       let _, pv = Proofview.init evm [] in
        let pv = Proofview.unshelve goals pv in
        try
          let (), pv', (unsafe, shelved, gaveup), _ =
@@ -964,7 +954,13 @@ module Search = struct
                       acc && okev) evm' true);
            let fgoals = Evd.shelve_on_future_goals shelved fgoals in
            let evm' = Evd.restore_future_goals evm' fgoals in
+           let nongoals' =
+             Evar.Set.fold (fun ev acc -> match Evarutil.advance evm' ev with
+                 | Some ev' -> Evar.Set.add ev acc
+                 | None -> acc) nongoals (Evd.get_typeclass_evars evm')
+           in
            let evm' = evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm in
+           let evm' = Evd.set_typeclass_evars evm' nongoals' in
            Some evm'
          else raise Not_found
        with Logic_monad.TacticFailure _ -> raise Not_found
@@ -1016,7 +1012,7 @@ let deps_of_constraints cstrs evm p =
 let evar_dependencies pred evm p =
   Evd.fold_undefined
     (fun ev evi _ ->
-      if Evd.is_resolvable_evar evm ev && pred evm ev evi then
+      if Evd.is_typeclass_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 ())
@@ -1032,8 +1028,7 @@ let split_evars pred evm =
 
 let is_inference_forced p evd ev =
   try
-    let evi = Evd.find_undefined evd ev in
-    if Evd.is_resolvable_evar evd ev && snd (p ev evi)
+    if Evar.Set.mem ev (Evd.get_typeclass_evars evd) && p ev
     then
       let (loc, k) = evar_source ev evd in
       match k with
@@ -1065,55 +1060,32 @@ let error_unresolvable env comp evd =
   Pretype_errors.unsatisfiable_constraints env evd ev comp
 
 (** Check if an evar is concerned by the current resolution attempt,
-    (and in particular is in the current component), and also update
-    its evar_info.
-    Invariant : this should only be applied to undefined evars,
-    and return undefined evar_info *)
+    (and in particular is in the current component).
+    Invariant : this should only be applied to undefined evars. *)
 
-let select_and_update_evars p oevd in_comp evd ev evi =
-  assert (evi.evar_body == Evar_empty);
+let select_and_update_evars p oevd in_comp evd ev =
   try
-    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 evd, false
-  with Not_found ->
-    Evd.set_resolvable_evar evd ev false, p evd ev evi
+    if Evd.is_typeclass_evar oevd ev then
+      (in_comp ev && p evd ev (Evd.find evd ev))
+    else false
+  with Not_found -> false
 
 (** Do we still have unresolved evars that should be resolved ? *)
 
 let has_undefined p oevd evd =
-  let check ev evi = snd (p oevd ev evi) in
+  let check ev evi = p oevd ev in
   Evar.Map.exists check (Evd.undefined_map evd)
 
-(** Revert the resolvability status of evars after resolution,
-    potentially unprotecting some evars that were set unresolvable
-    just for this call to resolution. *)
-
-let revert_resolvability oevd evd =
-  let fold ev _evi evd =
-    try
-      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.fold_undefined fold evd evd
-
 exception Unresolved
 
 (** If [do_split] is [true], we try to separate the problem in
     several components and then solve them separately *)
 let resolve_all_evars debug depth unique env p oevd do_split fail =
-  let split = if do_split then split_evars p oevd else [Evar.Set.empty] in
-  let in_comp comp ev = if do_split then Evar.Set.mem ev comp else true
-  in
+  let tcs = Evd.get_typeclass_evars oevd in
+  let split = if do_split then split_evars p oevd else [tcs] in
+  let in_comp comp ev = if do_split then Evar.Set.mem ev comp else true in
   let rec docomp evd = function
-    | [] -> revert_resolvability oevd evd
+    | [] -> evd
     | comp :: comps ->
       let p = select_and_update_evars p oevd (in_comp comp) in
       try
@@ -1131,7 +1103,9 @@ let resolve_all_evars debug depth unique env p oevd do_split fail =
 
 let initial_select_evars filter =
   fun evd ev evi ->
-    filter ev (snd evi.Evd.evar_source) &&
+    filter ev (Lazy.from_val (snd evi.Evd.evar_source)) &&
+    (** Typeclass evars can contain evars whose conclusion is not
+        yet determined to be a class or not. *)
     Typeclasses.is_class_evar evd evi
 
 let resolve_typeclass_evars debug depth unique env evd filter split fail =
@@ -1223,5 +1197,6 @@ let autoapply c i =
     unify_e_resolve false flags gl
                                  ((c,cty,Univ.ContextSet.empty),0,ce) <*>
       Proofview.tclEVARMAP >>= (fun sigma ->
-      let sigma = Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals sigma in
+      let sigma = Typeclasses.make_unresolvables
+          (fun ev -> Typeclasses.all_goals ev (Lazy.from_val (snd (Evd.find sigma ev).evar_source))) sigma in
       Proofview.Unsafe.tclEVARS sigma) end
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 50febdf448..ca77e03707 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -773,12 +773,13 @@ let pr_constraints printenv env sigma evars cstrs =
 
 let explain_unsatisfiable_constraints env sigma constr comp =
   let (_, constraints) = Evd.extract_all_conv_pbs sigma in
+  let tcs = Evd.get_typeclass_evars sigma in
   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 _ = match comp with
-  | None -> Evd.is_resolvable_evar sigma evk
-  | Some comp -> Evd.is_resolvable_evar sigma evk && Evar.Set.mem evk comp
+  | None -> Evar.Set.mem evk tcs
+  | Some comp -> Evar.Set.mem evk tcs && Evar.Set.mem evk comp
   in
   let undef = 
     let m = Evar.Map.filter is_kept undef in
-- 
cgit v1.2.3