diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-10-14 16:40:53 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-10-14 16:41:57 +0200 |
| commit | db80daaf82a08a1475c65f7c82bffb63c7efd27a (patch) | |
| tree | 7434552be2f13b230c4e27a865ddfeb154355aa5 /kernel/reduction.ml | |
| parent | 36f669f769fa23eb897adfa0450875a3c0db3476 (diff) | |
Temporary fix: kernel conversion needs to ignore l2r flag.
Stdlib does not compile when l2r flag is actually taken into account. We should
investigate...
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 68783780d..ccea06c76 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -740,7 +740,7 @@ let vm_conv cv_pb env t1 t2 = let default_conv cv_pb ?(l2r=false) env t1 t2 = try - fconv cv_pb l2r (fun _ -> None) env t1 t2 + fconv cv_pb false (fun _ -> None) env t1 t2 with Not_found | Invalid_argument _ -> (* If compilation fails, fall-back to closure conversion *) fconv cv_pb false (fun _->None) env t1 t2 |