From 193c6427645d960f195ab58872ed28301c76b0f3 Mon Sep 17 00:00:00 2001
From: gregoire
Date: Mon, 5 Dec 2005 17:52:50 +0000
Subject: correction bug 881.

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

(limited to 'kernel')

diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 921cd71284..f038c04f13 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -459,7 +459,9 @@ and nf_stk env c t stk  =
 	      mkLambda(name,dom,body)
           | _, _ -> nf_val env v crazy_type
 	in 
-	let aux = nf_predicate env (type_of_switch sw) mip.mind_nf_arity in
+	let aux = 
+	  nf_predicate env (type_of_switch sw) 
+	    (hnf_prod_applist env mip.mind_nf_arity (Array.to_list params)) in
 	!dep,aux in
       (* Calcul du type des branches *)
       let btypes = 
-- 
cgit v1.2.3