From f468e43f60f433f0f3f60d394d617072d0aed143 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 8 Dec 2009 11:06:29 +0000
Subject: Declaremods.ml: a useless function wrongly introduced in last commit

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

(limited to 'library/declaremods.ml')

diff --git a/library/declaremods.ml b/library/declaremods.ml
index 62b78af93..97047ebd7 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -897,11 +897,6 @@ let get_includeself_substobjs env objs me is_mod =
     ([],mp_self,subst_objects subst objects)
   with NothingToDo -> objs
 
-let id_of_mp = function
-  | MPfile dir -> List.hd (repr_dirpath dir)
-  | MPbound mbid -> id_of_mbid mbid
-  | MPdot (_,l) -> id_of_label l
-
 let declare_one_include interp_struct me_ast is_mod =
   let env = Global.env() in
   let me = interp_struct env me_ast in
-- 
cgit v1.2.3