aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar gregoire <gregoire@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-12-05 17:52:50 +0000
committerGravatar gregoire <gregoire@85f007b7-540e-0410-9357-904b9bb8a0f7>2005-12-05 17:52:50 +0000
commit193c6427645d960f195ab58872ed28301c76b0f3 (patch)
treea868cd0cb0a94e40e9b41b456c64c25a2d88c5d6
parenta3508843fa932cbc9a3c0b0d3dc5004752d2a8e4 (diff)
correction bug 881.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7641 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--kernel/vconv.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 921cd7128..f038c04f1 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 =