Merge PR #8741: [typeclasses] functionalize typeclass evar handling

7 files changed, 201 insertions, 93 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index f9d9ce3569..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 ?(store = Store.empty) ?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
@@ -427,34 +428,34 @@ 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 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 ?store ?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 ?store ?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 ?store ?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
     | 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 ?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
@@ -462,11 +463,11 @@ 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 ?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 =
@@ -714,7 +715,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..0c8d8c9b8a 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -27,8 +27,9 @@ 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 ->
+  ?typeclass_candidate:bool ->
   ?principal:bool ->
   named_context_val -> evar_map  -> types -> evar_map * EConstr.t
 
@@ -40,19 +41,21 @@ 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 ->
+  ?typeclass_candidate:bool ->
   ?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 ->
+  ?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. *)
@@ -77,7 +80,8 @@ 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 ->
+  ?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 eafdc4cb46..3a77a2b440 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;
+    typeclass_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
@@ -441,20 +444,82 @@ 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: typeclasses, restricted or obligation flag *)
+
+let get_typeclass_evars evd = evd.evar_flags.typeclass_evars
+
+let set_typeclass_evars evd tcs =
+  let flags = evd.evar_flags in
+  { evd with evar_flags = { flags with typeclass_evars = tcs } }
+
+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
+  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
+
+(** 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 =
+  { 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 }
 
 (** New evars *)
 
@@ -464,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 =
@@ -478,7 +543,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 +650,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;
+    typeclass_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 +707,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,24 +717,39 @@ 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 *)
-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
-  { evd with defn_evars; undf_evars; last_mods; evar_names }
+  { evd with defn_evars; undf_evars; last_mods; evar_names; evar_flags }
 
-let is_restricted_evar evi =
-  Store.get evi.evar_extra restricted
+(** 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
+
+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
@@ -679,9 +765,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_evar_flags 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 +1107,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..b0e3c2b869 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
@@ -145,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
@@ -182,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.}
@@ -190,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. *)
 
@@ -210,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
@@ -247,9 +247,27 @@ 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_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 get_typeclass_evars : evar_map -> Evar.Set.t
+(** The set of undefined typeclass evars *)
+
+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
+(** 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 +375,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..304b2dff84 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -60,19 +60,14 @@ 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 ~typeclass_candidate:false typ in
     let (gl, _) = EConstr.destEvar sigma econstr in
     let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
     let entry = (econstr, typ) :: ret in
@@ -745,26 +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
-  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
+      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
-  Evd.add evd content info
+  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
@@ -781,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)
 
@@ -1035,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
@@ -1043,9 +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 }
-
-  let typeclass_resolvable = typeclass_resolvable
+    { p with solution = mark_in_evm ~goal:false p.solution [gl] }
 
 end
 
@@ -1065,10 +1060,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 +1084,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..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
@@ -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..5e220fd8f1 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 typeclasses =
+    let evars = Evd.get_typeclass_evars sigma in
+    if Evar.Set.is_empty evars then mt ()
+    else
+      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 ++ metas
+  evs ++ svs ++ cstrs ++ typeclasses ++ metas
 
 let pr_evar_list sigma l =
   let open Evd in