- Fix bug #1858, Hint Unfold calling the wrong locate function.

- Fix typeclass interface: instance_constructor now takes the instance
  constrs as argument to build and return the corresponding term and
  type.
- Better typeclass error reporting when defining fixpoints.


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

3 files changed, 17 insertions, 10 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 765060b46c..a1b07cb9f2 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -226,12 +226,14 @@ let class_info c =
   try Gmap.find c !classes
   with _ -> not_a_class (Global.env()) (constr_of_global c)
 
-let instance_constructor cl = 
-  match cl.cl_impl with
-    | IndRef ind -> (fun args -> applistc (mkConstruct (ind, 1)) args), mkInd ind
-    | ConstRef cst -> list_last, mkConst cst
-    | _ -> assert false
-
+let instance_constructor cl args = 
+  let pars = fst (list_chop (List.length cl.cl_context) args) in
+    match cl.cl_impl with
+      | IndRef ind -> applistc (mkConstruct (ind, 1)) args,
+	  applistc (mkInd ind) pars
+      | ConstRef cst -> list_last args, applistc (mkConst cst) pars
+      | _ -> assert false
+	  
 let typeclasses () = Gmap.fold (fun _ l c -> l :: c) !classes []
 
 let cmapl_add x y m =
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index c6763a4213..43ae592d5c 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -60,8 +60,9 @@ val is_class : global_reference -> bool
 val class_of_constr : constr -> typeclass option
 val dest_class_app : constr -> typeclass * constr array (* raises a UserError if not a class *)
 
-(* Returns the constructor for the given fields of the class and the type constructor. *)
-val instance_constructor : typeclass -> (constr list -> constr) * types
+(* Returns the term and type for the given instance of the parameters and fields
+   of the type class. *)
+val instance_constructor : typeclass -> constr list -> constr * types
 
 val resolve_one_typeclass : env -> types -> types (* Raises Not_found *)
 val resolve_one_typeclass_evd : env -> evar_defs ref -> types -> types (* Raises Not_found *)
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index dc3f81f56f..aed42aa04d 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id:$ i*)
+(*i $Id$ i*)
 
 (*i*)
 open Names
@@ -41,6 +41,10 @@ let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id))
 
 let no_instance env id args = typeclass_error env (NoInstance (id, args))
 
-let unsatisfiable_constraints env evm = typeclass_error env (UnsatisfiableConstraints evm)
+let unsatisfiable_constraints env evd = 
+  let evd = Evd.undefined_evars evd in
+  let ev = List.hd (Evd.dom (Evd.evars_of evd)) in
+  let loc, _ = Evd.evar_source ev evd in
+    raise (Stdpp.Exc_located (loc, TypeClassError (env, UnsatisfiableConstraints evd)))
 
 let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))