diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-20 16:31:09 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-09-20 16:31:09 +0000 |
commit | 6aeea41c8a94233cb8b3ae15db1b20c75397610e (patch) | |
tree | 07446933f33ed70d3cf11020e9b4187efad3df6d /library/nametab.ml | |
parent | 500e89caeb3cb614cf2d51a2765cc42d0e10fed0 (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-x | library/nametab.ml | 25 |
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 |