diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/univ.ml | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/kernel/univ.ml b/kernel/univ.ml index 8dd733911e..6d23d301e5 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -82,7 +82,6 @@ module HList = struct val hash : t -> int val nil : t val cons : elt -> t -> t - val is_nil : t -> bool val tip : elt -> t val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a val map : (elt -> elt) -> t -> t @@ -103,8 +102,6 @@ module HList = struct let hash = function Nil -> 0 | Cons (_, h, _) -> h - let is_nil = function Nil -> true | Cons _ -> false - let tip e = cons e nil let rec fold f l accu = match l with @@ -536,10 +533,6 @@ struct str "max(" ++ hov 0 (prlist_with_sep pr_comma (Expr.pr_with f) (to_list l)) ++ str ")" - - let atom l = match l with - | Cons (l, _, Nil) -> Some l - | _ -> None let is_level l = match l with | Cons (l, _, Nil) -> Expr.is_level l @@ -613,7 +606,6 @@ struct let sup x y = merge_univs x y let empty = nil - let is_empty = function Nil -> true | Cons _ -> false let exists = Huniv.exists |