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

10 files changed, 43 insertions, 16 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'
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index afae141b99..a2285015dc 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -128,6 +128,8 @@ let ppenv e = pp
 
 let pptac = (fun x -> pp(Pptactic.pr_glob_tactic (Global.env()) x))
 
+let ppinsts c = pp (pr_instance_gmap c)
+
 let ppobj obj = Format.print_string (Libobject.object_tag obj)
 
 let cnt = ref 0
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 8ef206649e..6119f5d1e7 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -527,3 +527,14 @@ let pr_assumptionset env s =
     in
     (Option.default (mt ()) vars) ++ (Option.default (mt ()) axioms)
 
+let cmap_to_list m = Cmap.fold (fun k v acc -> v :: acc) m []
+
+open Typeclasses
+
+let pr_instance i = 
+  pr_global (ConstRef (instance_impl i))
+    
+let pr_instance_gmap insts =
+  prlist_with_sep fnl (fun (gr, insts) ->
+    prlist_with_sep fnl pr_instance (cmap_to_list insts))
+    (Gmap.to_list insts)
diff --git a/parsing/printer.mli b/parsing/printer.mli
index 262826ac8c..a4e0cd570f 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -137,3 +137,5 @@ val set_printer_pr : printer_pr -> unit
 
 val default_printer_pr : printer_pr
 
+val pr_instance_gmap : (global_reference, Typeclasses.instance Names.Cmap.t) Gmap.t ->
+  Pp.std_ppcmds
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index e75be25f30..530fec6d10 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -111,13 +111,13 @@ let gmap_cmap_merge old ne =
     Gmap.fold (fun cl insts acc -> 
       let oldinsts = try Gmap.find cl old with Not_found -> Cmap.empty in
 	Gmap.add cl (cmap_union oldinsts insts) acc)
-      Gmap.empty ne
+      ne Gmap.empty
   in
     Gmap.fold (fun cl insts acc -> 
       if Gmap.mem cl ne' then acc
       else Gmap.add cl insts acc)
-      ne' old
-      
+      old ne'
+
 let add_instance_hint_ref = ref (fun id pri -> assert false)
 let register_add_instance_hint =
   (:=) add_instance_hint_ref
@@ -284,9 +284,14 @@ let add_instance i =
   add_instance_hint i.is_impl i.is_pri;
   update ()
 
+let all_instances () = 
+  Gmap.fold (fun k v acc -> 
+    Cmap.fold (fun k v acc -> v :: acc) v acc)
+    !instances []
+
 let instances r = 
   let cl = class_info r in instances_of cl
-
+    
 let method_typeclass ref = 
   match ref with 
     | ConstRef c -> 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 09f6a76968..f77be52932 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -45,6 +45,7 @@ type instance
 
 val instances : global_reference -> instance list
 val typeclasses : unit -> typeclass list
+val all_instances : unit -> instance list
 
 val add_class : typeclass -> unit
 
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 7240217990..3ffa8040d9 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -75,7 +75,7 @@ Arguments Scope respectful [type_scope type_scope signature_scope signature_scop
 
 Open Local Scope signature_scope.
 
-(** Pointwise lifting is just respect with leibnize equality on the left. *)
+(** Pointwise lifting is just respect with leibniz equality on the left. *)
 
 Definition pointwise_relation {A B : Type} (R : relation B) : relation (A -> B) := 
   fun f g => forall x : A, R (f x) (g x).
@@ -222,8 +222,8 @@ Program Instance trans_sym_contra_impl_morphism
     transitivity x0... symmetry...
   Qed.
 
-Program Instance equivalence_partial_app_morphism
-  [ Equivalence A R ] : Morphism (R ==> iff) (R x) | 1.
+Program Instance per_partial_app_morphism
+  [ PER A R ] : Morphism (R ==> iff) (R x) | 1.
 
   Next Obligation.
   Proof with auto.
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index bcd4b92d6c..5212e63814 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -309,13 +309,12 @@ Proof NZgt_wf.
 
 Theorem lt_wf_0 : well_founded lt.
 Proof.
-assert (H : relations_eq lt (fun n m : N => 0 <= n /\ n < m)).
+setoid_replace lt with (fun n m : N => 0 <= n /\ n < m) 
+  using relation (@relations_eq N N).
+apply lt_wf.
 intros x y; split.
 intro H; split; [apply le_0_l | assumption]. now intros [_ H].
-rewrite H; apply lt_wf.
-(* does not work:
-setoid_replace lt with (fun n m : N => 0 <= n /\ n < m) using relation relations_eq.*)
-Qed.
+Defined.
 
 (* Theorems that are true for natural numbers but not for integers *)