Nettoyage des commentaires

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

5 files changed, 1 insertions, 63 deletions

diff --git a/kernel/closure.mli b/kernel/closure.mli
index e755f28d98..b7ded4a9f9 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -32,18 +32,6 @@ type evaluable_global_reference =
   Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of 
   a LetIn expression is Letin reduction *)
 
-(*
-type red_kind = 
-  | BETA
-  | DELTA
-  | ZETA
-  | EVAR
-  | IOTA
-  | CONST of section_path list
-  | CONSTBUT of section_path list
-  | VAR of identifier
-  | VARBUT of identifier
-*)
 (* Sets of reduction kinds. *)
 module type RedFlagsSig = sig
   type reds
diff --git a/kernel/univ.mli b/kernel/univ.mli
index e677b765ce..da66f4aed5 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -16,15 +16,9 @@ open Names
 
 type universe
 
-(*
-val dummy_univ : universe
-*)
 val implicit_univ : universe
 
 val prop_univ : universe
-(*
-val prop_univ_univ : universe
-*)
 
 val set_module : dir_path -> unit
 
@@ -38,11 +32,7 @@ val initial_universes : universes
 
 (*s Constraints. *)
 
-(*
-type constraint_type = Gt | Geq | Eq
-*)
-
-type univ_constraint (* = universe * constraint_type * universe *)
+type univ_constraint
 
 module Constraint : Set.S with type elt = univ_constraint
 
@@ -50,9 +40,6 @@ type constraints = Constraint.t
 
 type constraint_function = universe -> universe -> constraints -> constraints
 
-(*
-val enforce_gt : constraint_function
-*)
 val enforce_geq : constraint_function
 val enforce_eq : constraint_function
 
diff --git a/library/declare.mli b/library/declare.mli
index 4d7043eae7..8d5744ad22 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 979c9f2dc6..6cd43c392d 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 f525d49c7a..0ae357c9c4 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