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

1 files changed, 10 insertions, 8 deletions

diff --git a/library/globnames.ml b/library/globnames.ml
index 06a8f823d..e63fa64d5 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -142,6 +142,10 @@ let encode_mind dir id = make_mind (MPfile dir) Dir_path.empty (Label.of_id id)
 
 let encode_con dir id = make_con (MPfile dir) Dir_path.empty (Label.of_id id)
 
+let check_empty_section dp =
+  if not (Dir_path.is_empty dp) then
+    anomaly (Pp.str "Section part should be empty!")
+
 let decode_mind kn =
   let rec dir_of_mp = function
     | MPfile dir -> Dir_path.repr dir
@@ -152,17 +156,15 @@ let decode_mind kn =
     | MPdot(mp,l) -> (Label.to_id l)::(dir_of_mp mp)
   in
   let mp,sec_dir,l = repr_mind kn in
-    if (Dir_path.repr sec_dir) = [] then
-     (Dir_path.make (dir_of_mp mp)),Label.to_id l
-    else
-      anomaly (Pp.str "Section part should be empty!")
+  check_empty_section sec_dir;
+  (Dir_path.make (dir_of_mp mp)),Label.to_id l
 
 let decode_con kn =
   let mp,sec_dir,l = repr_con kn in
-    match mp,(Dir_path.repr sec_dir) with
-	MPfile dir,[] -> (dir,Label.to_id l)
-      | _ , [] -> anomaly (Pp.str "MPfile expected!")
-      | _ -> anomaly (Pp.str "Section part should be empty!")
+  check_empty_section sec_dir;
+  match mp with
+    | MPfile dir -> (dir,Label.to_id l)
+    | _ -> anomaly (Pp.str "MPfile expected!")
 
 (* popping one level of section in global names *)