From 2145e0274482017dc8e16c8ee774bc422be930e1 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Mon, 24 Feb 2014 11:39:18 +0100
Subject: univ: removing dead code

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

diff --git a/kernel/univ.ml b/kernel/univ.ml
index 44d487c1a5..062196b395 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -892,10 +892,6 @@ let sort_universes orig =
 
 (* Temporary inductive type levels *)
 
-let fresh_level =
-  let n = ref 0 in
-  fun () -> incr n; UniverseLevel.Level (!n, Names.DirPath.empty)
-
 let fresh_local_univ, set_remote_fresh_local_univ =
   RemoteCounter.new_counter 0 ~incr:((+) 1)
     ~build:(fun n -> Atom (UniverseLevel.Level (n, Names.DirPath.empty)))
-- 
cgit v1.2.3