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

12 files changed, 50 insertions, 16 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index 24879f41d6..da8a778837 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -349,6 +349,10 @@ let same_kind c1 c2 = (isprop c1 & isprop c2) or (is_Type c1 & is_Type c2)
 (* Tests if an evar *)
 let isEvar c = match kind_of_term c with Evar _ -> true | _ -> false
 
+let isEvar_or_Meta c = match kind_of_term c with 
+  | Evar _ | Meta _ -> true
+  | _ -> false
+
 (* Destructs a casted term *)
 let destCast c = match kind_of_term c with 
   | Cast (t1,k,t2) -> (t1,k,t2)
diff --git a/kernel/term.mli b/kernel/term.mli
index 6a6a4ad287..8f45e39f09 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -227,6 +227,7 @@ val isVar  : constr -> bool
 val isInd  : constr -> bool
 val isEvar : constr -> bool
 val isMeta : constr -> bool
+val isEvar_or_Meta : constr -> bool
 val isSort : constr -> bool
 val isCast : constr -> bool
 val isApp : constr -> bool
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 79c347cea6..8bf95ecbfb 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -310,8 +310,6 @@ let outCanonicalStructure x = fst (outCanonStruct x)
 let lookup_canonical_conversion (proj,pat) =
   List.assoc pat (Refmap.find proj !object_table)
 
-let isEvar_or_Meta c = isEvar c || isMeta c
-
 let is_open_canonical_projection sigma (c,args) =
   try 
     let l = Refmap.find (global_of_constr c) !object_table in
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index fc43628752..6a193e910a 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
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 3f0723ad85..b977a1a345 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -42,3 +42,5 @@ val no_instance : env -> identifier located -> constr list -> 'a
 val unsatisfiable_constraints : env -> evar_defs -> evar option -> 'a
 
 val mismatched_ctx_inst : env -> contexts -> constr_expr list -> rel_context -> 'a
+
+val unsatisfiable_exception : exn -> bool
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 4d0308c20f..269fb77df8 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -127,18 +127,21 @@ type unify_flags = {
   modulo_conv_on_closed_terms : Names.transparent_state option;
   use_metas_eagerly : bool;
   modulo_delta : Names.transparent_state;
+  resolve_evars : bool;
 }
 
 let default_unify_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
   use_metas_eagerly = true;
   modulo_delta = full_transparent_state;
+  resolve_evars = false;
 }
 
 let default_no_delta_unify_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
   use_metas_eagerly = true;
   modulo_delta = empty_transparent_state;
+  resolve_evars = false;
 }
 
 let expand_key env = function
@@ -308,14 +311,18 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	      solve_canonical_projection curenvnb pb b cM f1l1 cN f2l2 substn
 	  else error_cannot_unify (fst curenvnb) sigma (cM,cN)
       else error_cannot_unify (fst curenvnb) sigma (cM,cN)
-    in try f1 () with e when precatchable_exception e -> 
-      if isApp cN then
-	let f2l2 = decompose_app cN in
-	  if is_open_canonical_projection sigma f2l2 then
-	    let f1l1 = decompose_app cM in
-	      solve_canonical_projection curenvnb pb b cN f2l2 cM f1l1 substn
+    in
+      if flags.modulo_conv_on_closed_terms = None then 
+	error_cannot_unify (fst curenvnb) sigma (cM,cN)
+      else
+	try f1 () with e when precatchable_exception e -> 
+	  if isApp cN then
+	    let f2l2 = decompose_app cN in
+	      if is_open_canonical_projection sigma f2l2 then
+		let f1l1 = decompose_app cM in
+		  solve_canonical_projection curenvnb pb b cN f2l2 cM f1l1 substn
+	      else error_cannot_unify (fst curenvnb) sigma (cM,cN)
 	  else error_cannot_unify (fst curenvnb) sigma (cM,cN)
-      else error_cannot_unify (fst curenvnb) sigma (cM,cN)
 
   and solve_canonical_projection curenvnb pb b cM f1l1 cN f2l2 (sigma,ms,es) =
     let (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
@@ -665,8 +672,13 @@ let w_unify_meta_types env ?(flags=default_unify_flags) evd =
    types of metavars are unifiable with the types of their instances    *)
 
 let check_types env flags (sigma,_,_ as subst) m n =
-  if isEvar (fst (whd_stack sigma m)) or isEvar (fst (whd_stack sigma n)) then
-    unify_0_with_initial_metas subst true env topconv 
+  if isEvar_or_Meta (fst (whd_stack sigma m)) then
+    unify_0_with_initial_metas subst true env Cumul
+      flags
+      (Retyping.get_type_of env sigma n)
+      (Retyping.get_type_of env sigma m)
+  else if isEvar_or_Meta (fst (whd_stack sigma n)) then
+    unify_0_with_initial_metas subst true env Cumul
       flags
       (Retyping.get_type_of env sigma m)
       (Retyping.get_type_of env sigma n)
@@ -677,13 +689,17 @@ let w_unify_core_0 env with_types cv_pb flags m n evd =
   let (sigma,ms,es) = check_types env flags (evd,mc1,[]) m n in
   let subst2 =
      unify_0_with_initial_metas (evd',ms,es) true env cv_pb flags m n
-  in 
-  w_merge env with_types flags subst2
+  in
+  let evd = w_merge env with_types flags subst2 in
+    if flags.resolve_evars then 
+      try Typeclasses.resolve_typeclasses ~onlyargs:false ~split:true ~fail:true env evd
+      with e when Typeclasses_errors.unsatisfiable_exception e ->
+	error_cannot_unify env evd (m, n)
+    else evd
 
 let w_unify_0 env = w_unify_core_0 env false
 let w_typed_unify env = w_unify_core_0 env true
 
-
 (* takes a substitution s, an open term op and a closed term cl
    try to find a subterm of cl which matches op, if op is just a Meta
    FAIL because we cannot find a binding *)
@@ -762,7 +778,7 @@ let w_unify_to_subterm_list env flags allow_K oplist t evd =
     (fun op (evd,l) ->
       if isMeta op then
 	if allow_K then (evd,op::l)
-	else error "Match_subterm"
+	else error "Unify_to_subterm_list"
       else if occur_meta_or_existential op then
         let (evd',cl) =
           try 
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 1b8f9ccd8b..0e85f82436 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
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index e2bce9fde1..af118b5f1d 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)) *)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index aceb5c5250..8a2578c302 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -708,6 +708,7 @@ let auto_unif_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state; 
   use_metas_eagerly = false;
   modulo_delta = empty_transparent_state;
+  resolve_evars = true;
 }
 
 (* Try unification with the precompiled clause, then use registered Apply *)
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index f9485e64cd..78ef3c6fc8 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -103,6 +103,7 @@ let auto_unif_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state;
   use_metas_eagerly = true;
   modulo_delta = var_full_transparent_state;
+  resolve_evars = false;
 }
 
 let unify_e_resolve flags (c,clenv) gls = 
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 213f0d11e9..b981635eb7 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -272,6 +272,7 @@ let rewrite_unif_flags = {
   Unification.modulo_conv_on_closed_terms = None;
   Unification.use_metas_eagerly = true;
   Unification.modulo_delta = empty_transparent_state;
+  Unification.resolve_evars = true;
 }
 
 let conv_transparent_state = (Idpred.empty, Cpred.full)
@@ -280,6 +281,7 @@ let rewrite2_unif_flags = {
   Unification.modulo_conv_on_closed_terms = Some conv_transparent_state;
   Unification.use_metas_eagerly = true;
   Unification.modulo_delta = empty_transparent_state;
+  Unification.resolve_evars = true;
 }
 
 let convertible env evd x y =
@@ -320,7 +322,7 @@ let unify_eqn env sigma hypinfo t =
 		let mvs = clenv_dependent false env' in
 		  clenv_pose_metas_as_evars env' mvs
 	      in
-	      let evd' = Typeclasses.resolve_typeclasses ~fail:false env'.env env'.evd in
+	      let evd' = Typeclasses.resolve_typeclasses ~fail:true env'.env env'.evd in
 	      let env' = { env' with evd = evd' } in
 	      let nf c = Evarutil.nf_evar ( evd') (Clenv.clenv_nf_meta env' c) in
 	      let c1 = nf c1 and c2 = nf c2
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f3f15630fa..3d3b220457 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -680,6 +680,7 @@ let elim_flags = {
   modulo_conv_on_closed_terms = Some full_transparent_state; 
   use_metas_eagerly = true;
   modulo_delta = empty_transparent_state;
+  resolve_evars = false;
 }
 
 let elimination_clause_scheme with_evars allow_K elimclause indclause gl =