diff options
| author | Matthieu Sozeau | 2014-07-10 15:39:01 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-07-10 15:40:41 +0200 |
| commit | a071ac178ee9e6ca0cbae14db24e10775b0af881 (patch) | |
| tree | c732d20cb8ecd149300d60c2c69ba92432c84891 /kernel | |
| parent | 3abbc93733b7f820a436beedcd0b9292378e1840 (diff) | |
Overlooked to remove a change in kernel/closure that made reducing under
a primitive projection impossible.
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 _| |