diff options
| author | Maxime Dénès | 2015-10-16 13:20:19 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2015-10-16 13:36:04 +0200 |
| commit | d1ce79ce293c9b77f2c6a9d0b9a8b4f84ea617e5 (patch) | |
| tree | c21862745b135776c5d9b603d858fe04c045cf21 /kernel/reduction.mli | |
| 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.mli')
| -rw-r--r-- | kernel/reduction.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index b71356d033..c3cc7b2b69 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 *) |