Finer fix for bug 3017, mark unresolvability only of goals that are

instances of metas in clenvtac. Makes Math-Classes compile again.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16429 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 28 insertions, 17 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index d2cd0957e8..25109ffcf0 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -505,23 +505,27 @@ let mark_resolvability b evi =
 let mark_unresolvable evi = mark_resolvability false evi
 let mark_resolvable evi = mark_resolvability true evi
 
-let mark_resolvability b sigma =
-  Evd.fold_undefined (fun ev evi evs ->
-    Evd.add evs ev (mark_resolvability_undef b evi))
-    sigma (Evd.defined_evars sigma)
-
-let mark_unresolvables sigma = mark_resolvability false sigma
-let mark_resolvables sigma = mark_resolvability true sigma
-
 open Evar_kinds
 type evar_filter = Evar_kinds.t -> bool
 
 let all_evars _ = true
-let no_goals = function GoalEvar -> false | _ -> true
+let all_goals = function GoalEvar -> true | _ -> false
+let no_goals evi = not (all_goals evi)
 let no_goals_or_obligations = function
   | GoalEvar | QuestionMark _ -> false
   | _ -> true
 
+let mark_resolvability filter b sigma =
+  Evd.fold_undefined 
+    (fun ev evi evs ->
+     if filter (snd evi.evar_source) then
+       Evd.add evs ev (mark_resolvability_undef b evi)
+     else Evd.add evs ev evi)
+  sigma (Evd.defined_evars sigma)
+
+let mark_unresolvables ?(filter=all_evars) sigma = mark_resolvability filter false sigma
+let mark_resolvables sigma = mark_resolvability all_evars true sigma
+
 let has_typeclasses filter evd =
   Evd.fold_undefined (fun ev evi has -> has ||
     (filter (snd evi.evar_source) && is_class_evar evd evi && is_resolvable evi))
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 5e2b9b78d3..3f10200c03 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -77,22 +77,23 @@ val is_implicit_arg : Evar_kinds.t -> bool
 
 val instance_constructor : typeclass -> constr list -> constr option * types
 
+(** Filter which evars to consider for resolution. *)
+type evar_filter = Evar_kinds.t -> bool
+val all_evars : evar_filter
+val all_goals : evar_filter
+val no_goals : evar_filter
+val no_goals_or_obligations : evar_filter
+
 (** Resolvability.
     Only undefined evars can be marked or checked for resolvability. *)
 
 val is_resolvable : evar_info -> bool
 val mark_unresolvable : evar_info -> evar_info
-val mark_unresolvables : evar_map -> evar_map
+val mark_unresolvables : ?filter:evar_filter -> evar_map -> evar_map
 val mark_resolvable : evar_info -> evar_info
 val mark_resolvables : evar_map -> evar_map
 val is_class_evar : evar_map -> evar_info -> bool
 
-(** Filter which evars to consider for resolution. *)
-type evar_filter = Evar_kinds.t -> bool
-val all_evars : evar_filter
-val no_goals : evar_filter
-val no_goals_or_obligations : evar_filter
-
 val resolve_typeclasses : ?filter:evar_filter -> ?split:bool -> ?fail:bool ->
   env -> evar_map -> evar_map
 val resolve_one_typeclass : env -> evar_map -> types -> open_constr
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index b31d3a5fc9..389075c9ae 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -63,7 +63,7 @@ let clenv_refine with_evars ?(with_classes=true) clenv gls =
     if with_classes then
       let evd' = Typeclasses.resolve_typeclasses ~filter:Typeclasses.all_evars
         ~fail:(not with_evars) clenv.env clenv.evd
-      in Typeclasses.mark_unresolvables evd'
+      in Typeclasses.mark_unresolvables ~filter:Typeclasses.all_goals evd'
     else clenv.evd
   in
   let clenv = { clenv with evd = evd' } in
diff --git a/test-suite/bugs/closed/shouldsucceed/3017.v b/test-suite/bugs/closed/shouldsucceed/3017.v
new file mode 100644
index 0000000000..63a06bd3d6
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/3017.v
@@ -0,0 +1,6 @@
+Class A := {}.
+  Class B {T} `(A) := { B_intro : forall t t' : T, t = t' }.
+  Lemma foo T (t t' : T) : t = t'.
+    erewrite @B_intro.
+    reflexivity.
+  Abort.