diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/closure.mli | 1 | ||||
| -rw-r--r-- | kernel/constr.ml | 4 | ||||
| -rw-r--r-- | kernel/cooking.ml | 1 | ||||
| -rw-r--r-- | kernel/cooking.mli | 2 | ||||
| -rw-r--r-- | kernel/indtypes.mli | 2 | ||||
| -rw-r--r-- | kernel/modops.ml | 1 | ||||
| -rw-r--r-- | kernel/modops.mli | 1 | ||||
| -rw-r--r-- | kernel/names.ml | 3 | ||||
| -rw-r--r-- | kernel/nativeconv.ml | 4 | ||||
| -rw-r--r-- | kernel/nativeconv.mli | 2 | ||||
| -rw-r--r-- | kernel/nativelambda.mli | 3 | ||||
| -rw-r--r-- | kernel/nativelib.ml | 4 | ||||
| -rw-r--r-- | kernel/nativelib.mli | 4 | ||||
| -rw-r--r-- | kernel/reduction.mli | 1 | ||||
| -rw-r--r-- | kernel/retroknowledge.mli | 1 | ||||
| -rw-r--r-- | kernel/vconv.mli | 1 | ||||
| -rw-r--r-- | kernel/vm.mli | 1 |
17 files changed, 0 insertions, 36 deletions
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 *) |