diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-28 14:23:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-08-29 17:24:31 +0200 |
| commit | 37b81fe10d2da12180d96d931ba2b76370e1eea5 (patch) | |
| tree | 60559a7e8894147a4fb4884d854d9efb4e404a5b /kernel/mod_typing.ml | |
| parent | 1974816aca996fe3ee9420b83f11d15923e70fda (diff) | |
Statically enforcing that module types have no retroknowledge.
Diffstat (limited to 'kernel/mod_typing.ml')
| -rw-r--r-- | kernel/mod_typing.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index eead5b70d..d2b41aae9 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -283,9 +283,11 @@ let mk_mod mp e ty cst reso = mod_type_alg = None; mod_constraints = cst; mod_delta = reso; - mod_retroknowledge = [] } + mod_retroknowledge = ModBodyRK []; } -let mk_modtype mp ty cst reso = mk_mod mp () ty cst reso +let mk_modtype mp ty cst reso = + let mb = mk_mod mp Abstract ty cst reso in + { mb with mod_expr = (); mod_retroknowledge = ModTypeRK } let rec translate_mse_funct env mpo inl mse = function |[] -> @@ -321,6 +323,7 @@ let finalize_module env mp (sign,alg,reso,cst) restype = match restype with { res_mtb with mod_mp = mp; mod_expr = impl; + mod_retroknowledge = ModBodyRK []; (** cst from module body typing, cst' from subtyping, constraints from module type. *) |