diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2016-08-26 15:44:22 +0200 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-08-26 15:44:22 +0200 |
| commit | f70a374e05bd1235412ee7b76235b47d176ad595 (patch) | |
| tree | c071c04d08032caf67853af6f9c0484481dac9d9 /engine/termops.ml | |
| parent | ab9d2406975aba499d52f559e3303b82ce72d8ca (diff) | |
CLEANUP: removing "Termops.compact_named_context_reverse" function
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 1c2d261e5..501a7dfa4 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -982,7 +982,7 @@ let rec mem_named_context id ctxt = | _ :: sign -> mem_named_context id sign | [] -> false -let compact_named_context_reverse sign = +let compact_named_context sign = let compact l decl = match decl, l with | NamedDecl.LocalAssum (i,t), [] -> @@ -1002,9 +1002,7 @@ let compact_named_context_reverse sign = | NamedDecl.LocalDef (i,c,t), q -> CompactedDecl.LocalDef ([i],c,t) :: q in - Context.Named.fold_inside compact ~init:[] sign - -let compact_named_context sign = List.rev (compact_named_context_reverse sign) + Context.Named.fold_inside compact ~init:[] sign |> List.rev let clear_named_body id env = let open NamedDecl in |