Nettoyage des commentaires

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2031 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 0 insertions, 37 deletions

diff --git a/library/declare.mli b/library/declare.mli
index 4d7043eae..8d5744ad2 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -67,7 +67,6 @@ val declare_eliminations : mutual_inductive_path -> unit
 
 val out_inductive : Libobject.obj -> mutual_inductive_entry 
 
-(*val make_strength : dir_path -> strength*)
 val make_strength_0 : unit -> strength
 val make_strength_1 : unit -> strength
 val make_strength_2 : unit -> strength
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
diff --git a/library/nametab.mli b/library/nametab.mli
index f525d49c7..0ae357c9c 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -79,14 +79,7 @@ val locate_section : qualid -> dir_path
 (* [exists sp] tells if [sp] is already bound to a cci term *)
 val exists_cci : section_path -> bool
 val exists_section : dir_path -> bool
-(*
-val open_module_contents : qualid -> unit
-val rec_open_module_contents : qualid -> unit
 
-(*s Entry points for sections *)
-val open_section_contents : qualid -> unit
-val push_section : section_path -> module_contents -> unit
-*)
 (*s Roots of the space of absolute names *)
 
 (* This is the root of the standard library of Coq *)
@@ -103,10 +96,6 @@ val push_library_root : module_ident -> unit
    references inside a block of mutual inductive *)
 val absolute_reference : section_path -> global_reference
 
-(*
-val is_absolute_dirpath : dir_path -> bool
-*)
-
 (* [locate_in_absolute_module dir id] finds [id] in module [dir] or in
    one of its section/subsection *)
 val locate_in_absolute_module : dir_path -> identifier -> global_reference