From 14fdc212d664df129e2f718ea8b8eb87927a8ee8 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 22 Apr 2013 14:39:00 +0000
Subject: Declaremods: some more minor cleanup

 Some code cleaning and factorisation , comments, indentations, ...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16440 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/libnames.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'library/libnames.ml')

diff --git a/library/libnames.ml b/library/libnames.ml
index 43ece3417..bc2406f27 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -72,8 +72,8 @@ let dirpath_of_string s =
 
 let string_of_dirpath = Names.DirPath.to_string
 
-module Dirset = Set.Make(struct type t = DirPath.t let compare = DirPath.compare end)
-module Dirmap = Map.Make(struct type t = DirPath.t let compare = DirPath.compare end)
+module Dirset = Set.Make(DirPath)
+module Dirmap = Map.Make(DirPath)
 
 (*s Section paths are absolute names *)
 
@@ -81,14 +81,17 @@ type full_path = {
   dirpath : DirPath.t ;
   basename : Id.t }
 
-let eq_full_path p1 p2 =
-  Id.equal p1.basename p2.basename &&
-  DirPath.equal p1.dirpath p2.dirpath
+let dirpath sp = sp.dirpath
+let basename sp = sp.basename
 
 let make_path pa id = { dirpath = pa; basename = id }
 
 let repr_path { dirpath = pa; basename = id } = (pa,id)
 
+let eq_full_path p1 p2 =
+  Id.equal p1.basename p2.basename &&
+  DirPath.equal p1.dirpath p2.dirpath
+
 (* parsing and printing of section paths *)
 let string_of_path sp =
   let (sl,id) = repr_path sp in
@@ -110,9 +113,6 @@ module SpOrdered =
 
 module Spmap = Map.Make(SpOrdered)
 
-let dirpath sp = let (p,_) = repr_path sp in p
-let basename sp = let (_,id) = repr_path sp in id
-
 let path_of_string s =
   try
     let dir, id = split_dirpath (dirpath_of_string s) in
-- 
cgit v1.2.3