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/pretyping/unification.mli b/pretyping/unification.mli
index 1b8f9ccd8..0e85f8243 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -18,6 +18,7 @@ type unify_flags = {
   modulo_conv_on_closed_terms : Names.transparent_state option; 
   use_metas_eagerly : bool;
   modulo_delta : Names.transparent_state;
+  resolve_evars : bool;
 }
 
 val default_unify_flags : unify_flags