Remove some more "open" and dead code thanks to OCaml4 warnings

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

9 files changed, 2 insertions, 22 deletions

diff --git a/library/declaremods.ml b/library/declaremods.ml
index a61e59d6d3..fef95bc617 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -15,7 +15,6 @@ open Entries
 open Libnames
 open Libobject
 open Lib
-open Nametab
 open Mod_subst
 
 (** Rigid / flexible signature *)
diff --git a/library/dischargedhypsmap.ml b/library/dischargedhypsmap.ml
index 9dbbc947df..c26f652dfa 100644
--- a/library/dischargedhypsmap.ml
+++ b/library/dischargedhypsmap.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
 open Libnames
 
 type discharged_hyps = full_path list
diff --git a/library/global.ml b/library/global.ml
index 2d958f799f..c2bd551284 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
 open Names
 open Term
 open Environ
diff --git a/library/globnames.ml b/library/globnames.ml
index 27683278bb..8d298bc949 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Errors
-open Util
 open Names
 open Term
 open Mod_subst
diff --git a/library/goptions.ml b/library/goptions.ml
index a78ca750da..2a97f6149b 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -199,8 +199,6 @@ type 'a option_sig = {
   optread  : unit -> 'a;
   optwrite : 'a -> unit }
 
-type option_type = bool * (unit -> option_value) -> (option_value -> unit)
-
 module OptionMap =
   Map.Make (struct  type t = option_name let compare = compare end)
 
diff --git a/library/impargs.ml b/library/impargs.ml
index cc4a4e45ef..767e0e73a4 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -377,8 +377,6 @@ let compute_semi_auto_implicits env f manual t =
       let _,autoimpls = compute_auto_implicits env f f.auto t in
       [DefaultImpArgs, set_manual_implicits env f f.auto autoimpls manual]
 
-let compute_implicits env t = compute_semi_auto_implicits env !implicit_args [] t
-
 (*s Constants. *)
 
 let compute_constant_implicits flags manual cst =
diff --git a/library/lib.ml b/library/lib.ml
index a8a9f0c268..688df5a0e5 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -166,13 +166,6 @@ let find_entry_p p =
   in
   find !lib_stk
 
-let find_split_p p =
-  let rec find = function
-    | [] -> raise Not_found
-    | ent::l -> if p ent then ent,l else find l
-  in
-  find !lib_stk
-
 let split_lib_gen test =
   let rec collect after equal = function
     | hd::before when test hd -> collect after (hd::equal) before
@@ -571,12 +564,10 @@ let set_lib_stk new_lib_stk =
   with
     | Not_found -> error "Tried to set environment to an incoherent state."
 
-let reset_to_gen test =
+let reset_to test =
   let (_,_,before) = split_lib_gen test in
   set_lib_stk before
 
-let reset_to sp = reset_to_gen (fun x -> fst x = sp)
-
 let first_command_label = 1
 
 let mark_end_of_command, current_command_label, reset_command_label =
@@ -599,7 +590,7 @@ let is_label_n n x =
 let reset_label n =
   if n >= current_command_label () then
     error "Cannot backtrack to the current label or a future one";
-  reset_to_gen (is_label_n n);
+  reset_to (is_label_n n);
   (* forget state numbers after n only if reset succeeded *)
   reset_command_label n
 
diff --git a/library/libobject.ml b/library/libobject.ml
index 18b4c0c654..ffd87ce806 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Errors
-open Util
 open Libnames
 open Mod_subst
 
diff --git a/library/library.ml b/library/library.ml
index 9c881e515d..7dfde63a7b 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -496,8 +496,6 @@ let rec_intern_library_from_file idopt f =
     which recursively loads its dependencies)
 *)
 
-type library_reference = dir_path list * bool option
-
 let register_library m =
   Declaremods.register_library
     m.library_name