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, 1 insertions, 0 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index e2bce9fde..af118b5f1 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -107,6 +107,7 @@ let fail_quick_unif_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state; 
   use_metas_eagerly = false;
   modulo_delta = empty_transparent_state;
+  resolve_evars = false;
 }
 
 (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)