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 | |
| 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.
| -rw-r--r-- | kernel/reduction.ml | 6 | ||||
| -rw-r--r-- | kernel/reduction.mli | 2 |
2 files changed, 1 insertions, 7 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 diff --git a/kernel/reduction.mli b/kernel/reduction.mli index b71356d03..c3cc7b2b6 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -10,8 +10,6 @@ open Term open Context open Environ -val left2right : bool ref - (*********************************************************************** s Reduction functions *) |