Minor unification changes:

- Primitive setup for firing typeclass resolution on-demand: add a flag to
control resolution of remaining evars (e.g. typeclasses) during
unification. 
- Prevent canonical projection resolution when no delta is allowed
during unification (fixes incompatibility found in ssreflect).
- Correctly check types when the head is an evar _or_ a meta in w_unify.
  Move [isEvar_or_Meta] to kernel/term.ml, it's used in two places now.


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

1 files changed, 6 insertions, 0 deletions

diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index fc4362875..6a193e910 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -53,3 +53,9 @@ let unsatisfiable_constraints env evd ev =
 	    (env, UnsatisfiableConstraints (evd, Some (evi, kind)))))
 	    
 let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
+
+let rec unsatisfiable_exception exn =
+  match exn with
+  | TypeClassError (_, UnsatisfiableConstraints _) -> true
+  | Ploc.Exc (_, e) -> unsatisfiable_exception e
+  | _ -> false