diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-10-16 13:20:19 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-10-16 13:36:04 +0200 |
| commit | d1ce79ce293c9b77f2c6a9d0b9a8b4f84ea617e5 (patch) | |
| tree | c21862745b135776c5d9b603d858fe04c045cf21 /kernel/reduction.ml | |
| parent | 4dd61c9459a7388078bbd2e1b6f07959c4c72001 (diff) | |
Remove left2right reference from the kernel.
Was introduced by seemingly unrelated commit
fd62149f9bf40b3f309ebbfd7497ef7c185436d5.
The currently policy is to avoid exposing global references in the kernel
interface when easily doable.
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index c1f0008e6..2c111a55b 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -26,8 +26,6 @@ open Environ open Closure open Esubst -let left2right = ref false - let rec is_empty_stack = function [] -> true | Zupdate _::s -> is_empty_stack s @@ -210,9 +208,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv = let cu1 = cmp_rec s1 s2 cuniv in (match (z1,z2) with | (Zlapp a1,Zlapp a2) -> - if !left2right then - Array.fold_left2 (fun cu x y -> f x y cu) cu1 a1 a2 - else Array.fold_right2 f a1 a2 cu1 + Array.fold_right2 f a1 a2 cu1 | (Zlproj (c1,l1),Zlproj (c2,l2)) -> if not (eq_constant c1 c2) then raise NotConvertible |