aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine
diff options
context:
space:
mode:
authorGravatar Matej Kosik <m4tej.kosik@gmail.com>2016-08-30 10:47:37 +0200
committerGravatar Matej Kosik <m4tej.kosik@gmail.com>2016-08-30 10:47:37 +0200
commit2ff6d31c7a6011b26dfa7f0b2bb593b356833058 (patch)
tree82a3b37c697a2f4b2512cca8ebd72135dfb9673d /engine
parent24f70f4173726c5c4734a6f8f907d4bf4a0124ea (diff)
CLEANUP: using |> operator more consistently
Diffstat (limited to 'engine')
-rw-r--r--engine/termops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/termops.ml b/engine/termops.ml
index 501a7dfa4..b2c9492e1 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -1002,7 +1002,7 @@ let compact_named_context sign =
| NamedDecl.LocalDef (i,c,t), q ->
CompactedDecl.LocalDef ([i],c,t) :: q
in
- Context.Named.fold_inside compact ~init:[] sign |> List.rev
+ sign |> Context.Named.fold_inside compact ~init:[] |> List.rev
let clear_named_body id env =
let open NamedDecl in