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

8 files changed, 21 insertions, 48 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 95e908c4dd..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 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 ~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 ba4cde6d67..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 _ evi =
-    let res = Typeclasses.is_resolvable evi 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 c14c0a8a77..4e540de538 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,9 @@ 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, 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/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/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