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

---
 tactics/class_tactics.ml | 48 ++++++++++++++++++++++--------------------------
 tactics/eqdecide.ml      |  3 +--
 tactics/tactics.ml       | 43 +++++++++++++++++--------------------------
 3 files changed, 40 insertions(+), 54 deletions(-)

(limited to 'tactics')

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)
       ]
-- 
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
---
 tactics/autorewrite.ml   |   2 +-
 tactics/class_tactics.ml | 105 ++++++++++++++++++-----------------------------
 2 files changed, 41 insertions(+), 66 deletions(-)

(limited to 'tactics')

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
-- 
cgit v1.2.3