diff options
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index fa2384d47..72f577a7c 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -1008,15 +1008,19 @@ let hnf env sigma c = apprec env sigma (c, empty_stack) (* A reduction function like whd_betaiota but which keeps casts * and does not reduce redexes containing meta-variables. - * ASSUMES THAT APPLICATIONS ARE BINARY ONES. - * Used in Programs. + * Used in Correctness. * Added by JCF, 29/1/98. *) let whd_programs_stack env sigma = let rec whrec (x, stack as s) = match kind_of_term x with - | IsApp (f,([|c|] as cl)) -> - if occur_meta c then s else whrec (f, append_stack cl stack) + | IsApp (f,cl) -> + let n = Array.length cl - 1 in + let c = cl.(n) in + if occur_meta c then + s + else + whrec (mkApp (f, Array.sub cl 0 n), append_stack [|c|] stack) | IsLambda (_,_,c) -> (match decomp_stack stack with | None -> s |