From 48c844ddd8984b0eef6e9ec0aafefd28ccd03554 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 1 Jan 2010 23:25:49 +0000
Subject: Fix handling of instance declarations in presence of let-ins (bug
 reported by Eelis van der Weegen).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12618 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/typeclasses.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'pretyping/typeclasses.ml')

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 96e36b70ba..8d987d0379 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -272,7 +272,8 @@ let class_info c =
   with _ -> not_a_class (Global.env()) (constr_of_global c)
 
 let instance_constructor cl args =
-  let pars = fst (list_chop (List.length (fst cl.cl_context)) args) in
+  let lenpars = List.length (List.filter (fun (na, b, t) -> b = None) (snd cl.cl_context)) in
+  let pars = fst (list_chop lenpars args) in
     match cl.cl_impl with
       | IndRef ind -> applistc (mkConstruct (ind, 1)) args,
 	  applistc (mkInd ind) pars
-- 
cgit v1.2.3