aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/nametab.ml
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-09-20 16:31:09 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-09-20 16:31:09 +0000
commit6aeea41c8a94233cb8b3ae15db1b20c75397610e (patch)
tree07446933f33ed70d3cf11020e9b4187efad3df6d /library/nametab.ml
parent500e89caeb3cb614cf2d51a2765cc42d0e10fed0 (diff)
Nettoyage des commentaires
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2031 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/nametab.ml')
-rwxr-xr-xlibrary/nametab.ml25
1 files changed, 0 insertions, 25 deletions
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