diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-02 17:11:03 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-02 17:11:03 +0100 |
| commit | 80bbdf335be5657f5ab33b4aa02e21420d341de2 (patch) | |
| tree | 0fd5a807cecc57b6ce42c1b9a956d17f2ec5caeb /engine | |
| parent | 3f91296b5cf1dc9097d5368c2df5c6f70a04210c (diff) | |
Remove some unused functions.
Note: they do not even seem to have a debugging purpose, so better remove
them before they bitrot.
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/proofview_monad.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml index a9faf0a83..88c5925ce 100644 --- a/engine/proofview_monad.ml +++ b/engine/proofview_monad.ml @@ -108,11 +108,6 @@ module Info = struct and compress f = CList.map_filter compress_tree f - let rec is_empty = let open Trace in function - | Seq(Dispatch,brs) -> List.for_all is_empty brs - | Seq(DBranch,br) -> List.for_all is_empty br - | _ -> false - (** [with_sep] is [true] when [Tactic m] must be printed with a trailing semi-colon. *) let rec pr_tree with_sep = let open Trace in function |