From 648c594489f8d0ffdde9596b87f5c1ff6ccef612 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 18 Feb 2013 13:57:09 +0000
Subject: Minor code cleanups, especially take advantage of Dir_path.is_empty

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16210 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/univ.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/univ.ml b/kernel/univ.ml
index cfb7049323..9a27ff2a39 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -837,7 +837,8 @@ let sort_universes orig =
 (* Temporary inductive type levels *)
 
 let fresh_level =
-  let n = ref 0 in fun () -> incr n; UniverseLevel.Level (!n, Names.Dir_path.make [])
+  let n = ref 0 in
+  fun () -> incr n; UniverseLevel.Level (!n, Names.Dir_path.empty)
 
 let fresh_local_univ () = Atom (fresh_level ())
 
-- 
cgit v1.2.3