diff options
| author | gregoire | 2005-12-05 17:52:50 +0000 |
|---|---|---|
| committer | gregoire | 2005-12-05 17:52:50 +0000 |
| commit | 193c6427645d960f195ab58872ed28301c76b0f3 (patch) | |
| tree | a868cd0cb0a94e40e9b41b456c64c25a2d88c5d6 /kernel | |
| parent | a3508843fa932cbc9a3c0b0d3dc5004752d2a8e4 (diff) | |
correction bug 881.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7641 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/vconv.ml | 4 |
1 files changed, 3 insertions, 1 deletions
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 = |