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

2 files changed, 10 insertions, 4 deletions

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