diff options
Diffstat (limited to 'kernel/subtyping.ml')
| -rw-r--r-- | kernel/subtyping.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 961dd652f..5fec0c2c7 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -12,18 +12,15 @@ (* This module checks subtyping of module types *) (*i*) -open Errors open Util open Names open Univ open Term open Declarations -open Environ open Reduction open Inductive open Modops open Mod_subst -open Entries (*i*) (* This local type is used to subtype a constant with a constructor or |