diff options
Diffstat (limited to 'kernel')
| -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 b12b6502ac..586661d16f 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -942,7 +942,7 @@ let rec knh info m stk = | Some pb -> knh info c (Zproj (pb.Declarations.proj_npars, pb.Declarations.proj_arg, p) :: zupdate m stk)) - else (set_norm m; (m,stk)) + else (m,stk) (* cases where knh stops *) | (FFlex _|FLetIn _|FConstruct _|FEvar _| |