diff options
Diffstat (limited to 'kernel/vconv.ml')
| -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 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 = |