From adfd437f8ae6aaf893119fa4730edecf067dede7 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Wed, 5 Mar 2014 14:59:16 +0100
Subject: Remove many superfluous 'open' indicated by ocamlc -w +33

 With ocaml 4.01, the 'unused open' warning also checks the mli :-)

 Beware: some open are reported as useless when compiling with camlp5,
 but are necessary for compatibility with camlp4. These open are now
 marked with a comment.
---
 kernel/closure.mli        | 1 -
 kernel/constr.ml          | 4 ----
 kernel/cooking.ml         | 1 -
 kernel/cooking.mli        | 2 --
 kernel/indtypes.mli       | 2 --
 kernel/modops.ml          | 1 -
 kernel/modops.mli         | 1 -
 kernel/names.ml           | 3 ---
 kernel/nativeconv.ml      | 4 ----
 kernel/nativeconv.mli     | 2 --
 kernel/nativelambda.mli   | 3 ---
 kernel/nativelib.ml       | 4 ----
 kernel/nativelib.mli      | 4 ----
 kernel/reduction.mli      | 1 -
 kernel/retroknowledge.mli | 1 -
 kernel/vconv.mli          | 1 -
 kernel/vm.mli             | 1 -
 17 files changed, 36 deletions(-)

(limited to 'kernel')

diff --git a/kernel/closure.mli b/kernel/closure.mli
index 161de91cfa..19baedf276 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Pp
 open Names
 open Term
 open Environ
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 826c7f6437..cf05fe0139 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -23,12 +23,8 @@
    Inductive Constructions (CIC) terms together with constructors,
    destructors, iterators and basic functions *)
 
-open Errors
 open Util
-open Pp
 open Names
-open Univ
-open Esubst
 
 
 type existential_key = Evar.t
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index f8724180e4..31e86e8540 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -17,7 +17,6 @@ open Errors
 open Util
 open Names
 open Term
-open Context
 open Declarations
 open Environ
 
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 8493b81d82..030e888294 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -6,11 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
 open Term
 open Declarations
 open Environ
-open Univ
 
 (** {6 Cooking the constants. } *)
 
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index ce789b00eb..016a1a5b55 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -7,12 +7,10 @@
 (************************************************************************)
 
 open Names
-open Univ
 open Term
 open Declarations
 open Environ
 open Entries
-open Typeops
 
 (** Inductive type checking and errors *)
 
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 2bd421bb3c..188bff626d 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -15,7 +15,6 @@
 
 (* This file provides with various operations on modules and module types *)
 
-open Errors
 open Util
 open Names
 open Term
diff --git a/kernel/modops.mli b/kernel/modops.mli
index f50dcfd637..a71e28d6e4 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Univ
 open Term
 open Environ
 open Declarations
diff --git a/kernel/names.ml b/kernel/names.ml
index 047d8a88d6..3de12b1bc3 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -19,7 +19,6 @@
    Élie Soubiran, ... *)
 
 open Pp
-open Errors
 open Util
 
 (** {6 Identifiers } *)
@@ -485,8 +484,6 @@ module KerPair = struct
       the same user part implies having the same canonical part
       (invariant of the system). *)
 
-  open Hashset.Combine
-
   let hash = function
   | Same kn -> KerName.hash kn
   | Dual (kn, _) -> KerName.hash kn
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 3435e1d753..82786df64c 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -7,15 +7,11 @@
 (************************************************************************)
 open Errors
 open Names
-open Term
 open Univ
-open Pre_env
 open Nativelib
 open Reduction
-open Declarations
 open Util
 open Nativevalues
-open Nativelambda
 open Nativecode 
 
 (** This module implements the conversion test by compiling to OCaml code *)
diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli
index 2481300763..69b9d22ec7 100644
--- a/kernel/nativeconv.mli
+++ b/kernel/nativeconv.mli
@@ -6,8 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 open Term
-open Univ
-open Environ
 open Reduction
 open Nativelambda
 
diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli
index 860283e065..98314348ab 100644
--- a/kernel/nativelambda.mli
+++ b/kernel/nativelambda.mli
@@ -5,11 +5,8 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-open Util
 open Names
-open Esubst
 open Term
-open Declarations
 open Pre_env
 open Nativevalues
 
diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml
index f8c39b4dce..a69b9d472d 100644
--- a/kernel/nativelib.ml
+++ b/kernel/nativelib.ml
@@ -5,13 +5,9 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-open Names
-open Term
 open Util
 open Nativevalues
-open Declarations
 open Nativecode
-open Pre_env
 open Errors
 open Envars
 
diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli
index 0cbe4ccd5e..9ef8c06a31 100644
--- a/kernel/nativelib.mli
+++ b/kernel/nativelib.mli
@@ -5,11 +5,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-open Names
-open Term
-open Nativevalues
 open Nativecode
-open Pre_env
 
 (** This file provides facilities to access OCaml compiler and dynamic linker,
 used by the native compiler. *)
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 2d117cc96c..7c0607cc4d 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -9,7 +9,6 @@
 open Term
 open Context
 open Environ
-open Closure
 
 (***********************************************************************
   s Reduction functions *)
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 6b76e616aa..ea2b3de24f 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
 open Term
 
 type retroknowledge
diff --git a/kernel/vconv.mli b/kernel/vconv.mli
index 4168e50160..96ab5adecb 100644
--- a/kernel/vconv.mli
+++ b/kernel/vconv.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
 open Term
 open Environ
 open Reduction
diff --git a/kernel/vm.mli b/kernel/vm.mli
index cbc68c4884..fa88418cef 100644
--- a/kernel/vm.mli
+++ b/kernel/vm.mli
@@ -1,7 +1,6 @@
 open Names
 open Term
 open Cbytecodes
-open Cemitcodes
 
 (** Efficient Virtual Machine *)
 
-- 
cgit v1.2.3