diff options
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 7a41e62c47..c38d4186fb 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -20,6 +20,7 @@ (* This file defines the type of environments on which the type-checker works, together with simple related functions *) +open Errors open Util open Names open Sign |