diff options
Diffstat (limited to 'kernel/closure.ml')
| -rw-r--r-- | kernel/closure.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 2d30b2aa30..078f46b8d6 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -884,7 +884,7 @@ let rec knh m stk = | (None, stk') -> (m,stk')) | FCast(t,_) -> knh t stk (* cases where knh stops *) - | (FFlex _|FLetIn _|FInd _|FConstruct _|FEvar _) -> (m, stk) + | (FFlex _|FLetIn _|FConstruct _|FEvar _) -> (m, stk) | (FRel _|FAtom _|FInd _) -> (set_norm m; (m, stk)) | (FLambda _|FCoFix _|FProd _) -> (set_whnf m; (m, stk)) |