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
---
 interp/syntax_def.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index a07b6aa69c..bb3eeb2e08 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -42,7 +42,7 @@ let load_syntax_constant i ((sp,kn),(_,pat,onlyparse)) =
 let is_alias_of_already_visible_name sp = function
   | _,NRef ref ->
       let (dir,id) = repr_qualid (shortest_qualid_of_global Id.Set.empty ref) in
-      Dir_path.equal dir Dir_path.empty && Id.equal id (basename sp)
+      Dir_path.is_empty dir && Id.equal id (basename sp)
   | _ ->
       false
 
-- 
cgit v1.2.3