Better implementation of 4a858a51322f2dd488b02130ca82ebcc4dc9ca35.

Instead of filtering over the goals we have just creating and running through the evar_map, fetching the evar_info (that we've just created), and marking it as unresolvable, the goals are just created unresolvable. Which is probably what I should have done from the beginning, but it had escaped my notice during my code-cleaning session.

1 files changed, 5 insertions, 7 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index f5087b2c9..827fe56a6 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -55,11 +55,14 @@ type telescope =
   | TCons of Environ.env * Evd.evar_map * Term.types * (Evd.evar_map -> Term.constr -> telescope)
 
 let dependent_init =
+  (* Goals are created with a store which marks them as unresolvable
+     for type classes. *)
+  let store = Typeclasses.set_resolvable Evd.Store.empty false in
   let rec aux = function
   | TNil sigma -> [], { solution = sigma; comb = []; }
   | TCons (env, sigma, typ, t) ->
     let src = (Loc.ghost,Evar_kinds.GoalEvar) in
-    let (sigma, econstr ) = Evarutil.new_evar env sigma ~src typ in
+    let (sigma, econstr ) = Evarutil.new_evar env sigma ~src ~store typ in
     let ret, { solution = sol; comb = comb } = aux (t sigma econstr) in
     let (gl, _) = Term.destEvar econstr in
     let entry = (econstr, typ) :: ret in
@@ -67,13 +70,8 @@ let dependent_init =
   in
   fun t ->
     let entry, v = aux t in
-    (* Marks all the goal unresolvable for typeclasses. *)
-    let fold accu ev = Evar.Set.add ev accu in
-    let gls = List.fold_left fold Evar.Set.empty v.comb in
-    let filter evk _ = Evar.Set.mem evk gls in
-    let solution = Typeclasses.mark_unresolvables ~filter v.solution in
     (* The created goal are not to be shelved. *)
-    let solution = Evd.reset_future_goals solution in
+    let solution = Evd.reset_future_goals v.solution in
     entry, { v with solution }
 
 let init =