From 6aeea41c8a94233cb8b3ae15db1b20c75397610e Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 20 Sep 2001 16:31:09 +0000
Subject: Nettoyage des commentaires

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

(limited to 'library/nametab.ml')

diff --git a/library/nametab.ml b/library/nametab.ml
index 979c9f2dc..6cd43c392 100755
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -144,12 +144,6 @@ let push_cci n sp ref =
 
 let push = push_cci
 
-(*
-let push_short_name sp ref =
-  (* We push a volatile unqualified name *)
-  push_short_name_ccipath 0 [] (basename sp) (TrueGlobal ref)
-*)
-
 (* This is for Syntactic Definitions *)
 
 let push_syntactic_definition sp =
@@ -235,25 +229,6 @@ let constant_sp_of_id id =
     | TrueGlobal (ConstRef sp) -> sp
     | _ -> raise Not_found
 
-(*
-let check_absoluteness dir =
-  match dir with
-    | a::_ when List.mem a !roots -> ()
-    | _ -> anomaly ("Not an absolute dirpath: "^(string_of_dirpath dir))
-
-let is_absolute_dirpath = function
-    | a::_ when List.mem a !roots -> true
-    | _ -> false
-
-let absolute_reference sp =
-  check_absoluteness (dirpath sp);
-  locate (qualid_of_sp sp)
-
-let locate_in_absolute_module dir id =
-  check_absoluteness dir;
-  locate (make_qualid dir id)
-*)
-
 let absolute_reference sp =
   let a = locate_cci (qualid_of_sp sp) in
   if not (dirpath_of_extended_ref a = dirpath sp) then
-- 
cgit v1.2.3