diff options
Diffstat (limited to 'kernel/indtypes.mli')
| -rw-r--r-- | kernel/indtypes.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index ce789b00e..016a1a5b5 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 *) |