Fixing bug #3682.

The function initializing proofviews were marking all evars as non-resolvables
for the proofview, while only goal evars ought to be.

1 files changed, 4 insertions, 1 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index a8b77e225..1813c716e 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -68,7 +68,10 @@ let dependent_init =
   fun t ->
     let entry, v = aux t in
     (* Marks all the goal unresolvable for typeclasses. *)
-    let solution = Typeclasses.mark_unresolvables v.solution in
+    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
     entry, { v with solution }