diff options
| author | Matej Kosik | 2016-08-26 15:44:22 +0200 |
|---|---|---|
| committer | Matej Kosik | 2016-08-26 15:44:22 +0200 |
| commit | f70a374e05bd1235412ee7b76235b47d176ad595 (patch) | |
| tree | c071c04d08032caf67853af6f9c0484481dac9d9 /engine | |
| parent | ab9d2406975aba499d52f559e3303b82ce72d8ca (diff) | |
CLEANUP: removing "Termops.compact_named_context_reverse" function
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/termops.ml | 6 | ||||
| -rw-r--r-- | engine/termops.mli | 1 |
2 files changed, 2 insertions, 5 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 1c2d261e51..501a7dfa47 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 diff --git a/engine/termops.mli b/engine/termops.mli index bfd902f44a..a7f45d28ae 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -239,7 +239,6 @@ val fold_named_context_both_sides : Context.Named.t -> init:'a -> 'a val mem_named_context : Id.t -> Context.Named.t -> bool val compact_named_context : Context.Named.t -> Context.Compacted.t -val compact_named_context_reverse : Context.Named.t -> Context.Compacted.t val clear_named_body : Id.t -> env -> env |