From 8e1a7e3e6a4c84db18f6fd5334776489015b368d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 20 Dec 2014 17:06:06 +0100
Subject: Dead code in Univ.

---
 kernel/univ.ml | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'kernel')

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
 
-- 
cgit v1.2.3