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

5 files changed, 3 insertions, 31 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 2baea11a3..f49b1f375 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -70,16 +70,12 @@ module type VISIT = sig
   (* Reset the dependencies by emptying the visit lists *)
   val reset : unit -> unit
 
-  (* Add the module_path and all its prefixes to the mp visit list *)
-  val add_mp : module_path -> unit
-
-  (* Same, but we'll keep all fields of these modules *)
+  (* Add the module_path and all its prefixes to the mp visit list.
+     We'll keep all fields of these modules. *)
   val add_mp_all : module_path -> unit
 
-  (* Add kernel_name / constant / reference / ... in the visit lists.
+  (* Add reference / ... in the visit lists.
      These functions silently add the mp of their arg in the mp list *)
-  val add_ind : mutual_inductive -> unit
-  val add_con : constant -> unit
   val add_ref : global_reference -> unit
   val add_decl_deps : ml_decl -> unit
   val add_spec_deps : ml_spec -> unit
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 58e9a5220..bdb102b18 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -10,8 +10,6 @@
 
 (* ML names *)
 
-open Vernacexpr
-open Pcoq
 open Genarg
 open Pp
 open Names
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 4fd9f17ee..33da06f01 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -13,7 +13,6 @@ open Errors
 open Util
 open Names
 open Nameops
-open Libnames
 open Globnames
 open Table
 open Miniml
@@ -82,10 +81,6 @@ let pp_global k r =
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
     are needed or not. *)
 
-let kn_sig =
-  let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in
-  make_mind specif empty_dirpath (mk_label "sig")
-
 let rec pp_type par vl t =
   let rec pp_rec par = function
     | Tmeta _ | Tvar' _ -> assert false
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index e3abab82b..b53fec23e 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -224,21 +224,6 @@ let type_maxvar t =
     | _ -> n
   in parse 0 t
 
-(*s What are the type variables occurring in [t]. *)
-
-let intset_union_map_list f l =
-  List.fold_left (fun s t -> Intset.union s (f t)) Intset.empty l
-
-let intset_union_map_array f a =
-  Array.fold_left (fun s t -> Intset.union s (f t)) Intset.empty a
-
-let rec type_listvar = function
-  | Tmeta {contents = Some t} -> type_listvar t
-  | Tvar i | Tvar' i -> Intset.singleton i
-  | Tarr (a,b) -> Intset.union (type_listvar a) (type_listvar b)
-  | Tglob (_,l) -> intset_union_map_list type_listvar l
-  | _ -> Intset.empty
-
 (*s From [a -> b -> c] to [[a;b],c]. *)
 
 let rec type_decomp = function
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 9247baba2..4a390128a 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -289,8 +289,6 @@ and optim_me to_appear s = function
    For non-library extraction, we recompute a minimal set of dependencies
    for first-level objects *)
 
-exception NoDepCheck
-
 let base_r = function
   | ConstRef c as r -> r
   | IndRef (kn,_) -> IndRef (kn,0)