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/safe_typing.ml | |
| parent | 1974816aca996fe3ee9420b83f11d15923e70fda (diff) | |
Statically enforcing that module types have no retroknowledge.
Diffstat (limited to 'kernel/safe_typing.ml')
| -rw-r--r-- | kernel/safe_typing.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index aa26405f7..ad622b07d 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -677,7 +677,7 @@ let build_module_body params restype senv = (struc,None,senv.modresolver,senv.univ) restype' in let mb' = functorize_module params mb in - { mb' with mod_retroknowledge = senv.local_retroknowledge } + { mb' with mod_retroknowledge = ModBodyRK senv.local_retroknowledge } (** Returning back to the old pre-interactive-module environment, with one extra component and some updated fields @@ -737,7 +737,7 @@ let build_mtb mp sign cst delta = mod_type_alg = None; mod_constraints = cst; mod_delta = delta; - mod_retroknowledge = [] } + mod_retroknowledge = ModTypeRK } let end_modtype l senv = let mp = senv.modpath in @@ -853,7 +853,7 @@ let export ?except senv dir = mod_type_alg = None; mod_constraints = senv.univ; mod_delta = senv.modresolver; - mod_retroknowledge = senv.local_retroknowledge + mod_retroknowledge = ModBodyRK senv.local_retroknowledge } in let ast, symbols = |