From 4a858a51322f2dd488b02130ca82ebcc4dc9ca35 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 30 Nov 2014 02:23:57 +0100
Subject: Fixing bug #3682.

The function initializing proofviews were marking all evars as non-resolvables
for the proofview, while only goal evars ought to be.
---
 proofs/proofview.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index a8b77e225f..1813c716eb 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 }
-- 
cgit v1.2.3