diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-07-16 16:40:25 +0200 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-07-16 16:42:48 +0200 |
commit | ebb53e68cdc935a85c4da10852be4f7f3b492ee2 (patch) | |
tree | d2ce0abd3158e90aaf8076e13e57b436f4ea4b68 /kernel | |
parent | 3bcc96d5ab6571a7810b68c340af7aa195ef76f4 (diff) |
Modules: fix bug #4294
We were throwing away constraints from 'with Definition' in module
type ascriptions.
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/mod_typing.ml | 4 | ||||
-rw-r--r-- | kernel/univ.ml | 2 |
2 files changed, 4 insertions, 2 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 26dd45f5f..4f20e5f62 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -307,7 +307,9 @@ let finalize_module env mp (sign,alg,reso,cst) restype = match restype with { res_mtb with mod_mp = mp; mod_expr = impl; - mod_constraints = cst +++ cst' } + (** cst from module body typing, cst' from subtyping, + and constraints from module type. *) + mod_constraints = cst +++ cst' +++ res_mtb.mod_constraints } let translate_module env mp inl = function |MType (params,ty) -> diff --git a/kernel/univ.ml b/kernel/univ.ml index 1d82be63b..336cdb653 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -577,7 +577,7 @@ struct let is_type0m x = equal type0m x let is_type0 x = equal type0 x - (* Returns the formal universe that lies juste above the universe variable u. + (* Returns the formal universe that lies just above the universe variable u. Used to type the sort u. *) let super l = if is_small l then type1 |