diff options
| author | Pierre-Marie Pédrot | 2017-07-28 14:23:37 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-29 17:24:31 +0200 |
| commit | 37b81fe10d2da12180d96d931ba2b76370e1eea5 (patch) | |
| tree | 60559a7e8894147a4fb4884d854d9efb4e404a5b /checker/mod_checking.ml | |
| parent | 1974816aca996fe3ee9420b83f11d15923e70fda (diff) | |
Statically enforcing that module types have no retroknowledge.
Diffstat (limited to 'checker/mod_checking.ml')
| -rw-r--r-- | checker/mod_checking.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index de568e636b..3c9e1cac54 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -75,7 +75,7 @@ let mk_mtb mp sign delta = mod_type_alg = None; mod_constraints = Univ.ContextSet.empty; mod_delta = delta; - mod_retroknowledge = []; } + mod_retroknowledge = ModTypeRK; } let rec check_module env mp mb = let (_:module_signature) = |