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 --- library/globnames.ml | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) (limited to 'library/globnames.ml') 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 *) -- cgit v1.2.3