Various bug fixes in type classes and subtac:

- Cases on multiple objects
- Avoid dangerous coercion with evars in subtac_coercion
- Resolve typeclasses method-by-method to get better error messages.
- Correct merging of instance databases (and add debug printer)
- Fix a script in NOrder where a setoid_replace was not working before.


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

3 files changed, 11 insertions, 4 deletions

diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index c1b1283c63..009b806066 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -2056,8 +2056,10 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra
 	    t, prepare_predicate_from_arsign_tycon loc env (Evd.evars_of !isevars)
 	      tomatchs sign (lift tomatchs_len t)
       in
-      let arity = 
-	it_mkProd_or_LetIn (lift neqs arity) (context_of_arsign eqs)
+      let neqs, arity = 
+	let ctx = context_of_arsign eqs in
+	let neqs = List.length ctx in
+	  neqs, it_mkProd_or_LetIn (lift neqs arity) ctx
       in
       let lets, matx = 
 	(* Type the rhs under the assumption of equations *)
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 26cb416aca..efb99bdb0b 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -75,6 +75,7 @@ let type_ctx_instance isevars env ctx inst subst =
     (fun (subst, instctx) (na, _, t) ce ->
       let t' = substl subst t in
       let c = interp_casted_constr_evars isevars env ce t' in
+      isevars := resolve_typeclasses ~onlyargs:true ~fail:true env !isevars;
       let d = na, Some c, t' in
 	c :: subst, d :: instctx)
     (subst, []) (List.rev ctx) inst
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index 9c559e6cba..648b865c11 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -148,7 +148,11 @@ module Coercion = struct
 				      [| eqT; hdx; pred; x; hdy; evar|]) in
 		  aux (hdy :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i)  (fun x -> eq_app (co x))
 	  else Some co
-	in aux [] typ typ' 0 (fun x -> x)
+	in 
+	  if isEvar c || isEvar c' then
+	    (* Second-order unification needed. *)
+	    raise NoSubtacCoercion;
+	  aux [] typ typ' 0 (fun x -> x)
       in
 	match (kind_of_term x, kind_of_term y) with
 	  | Sort s, Sort s' -> 
@@ -485,7 +489,7 @@ module Coercion = struct
       try let rels, rng = decompose_prod_n nabs t in
 	(* The final range free variables must have been replaced by evars, we accept only that evars
 	   in rng are applied to free vars. *)
-	if noccur_with_meta 0 (succ nabs) rng then (
+	if noccur_with_meta 1 (succ nabs) rng then (
 	  let env', t, t' =
 	    let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in
 	      env', rng, lift nabs t'