diff options
Diffstat (limited to 'kernel/pre_env.mli')
| -rw-r--r-- | kernel/pre_env.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index b6d83b918..518c6330d 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -26,7 +26,8 @@ type globals = { env_constants : constant_key Cmap.t; env_inductives : mutual_inductive_body KNmap.t; env_modules : module_body MPmap.t; - env_modtypes : module_type_body MPmap.t } + env_modtypes : module_type_body MPmap.t; + env_alias : module_path MPmap.t } type stratification = { env_universes : universes; |