From 97f2cb04e369e07dc87dc15d4871b736776614bd Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 23 May 2008 11:47:43 +0000
Subject: - 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
---
 pretyping/typeclasses.ml | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

(limited to 'pretyping/typeclasses.ml')

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 =
-- 
cgit v1.2.3