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 /kernel/modops.ml | |
| parent | 1974816aca996fe3ee9420b83f11d15923e70fda (diff) | |
Statically enforcing that module types have no retroknowledge.
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 925d042b19..76915e917a 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -143,10 +143,12 @@ let rec functor_iter fty f0 = function (** {6 Misc operations } *) let module_type_of_module mb = - { mb with mod_expr = (); mod_type_alg = None } + { mb with mod_expr = (); mod_type_alg = None; + mod_retroknowledge = ModTypeRK; } let module_body_of_type mp mtb = - { mtb with mod_expr = Abstract; mod_mp = mp } + { mtb with mod_expr = Abstract; mod_mp = mp; + mod_retroknowledge = ModBodyRK []; } let check_modpath_equiv env mp1 mp2 = if ModPath.equal mp1 mp2 then () @@ -270,7 +272,7 @@ let add_retroknowledge mp = CErrors.anomaly ~label:"Modops.add_retroknowledge" (Pp.str "had to import an unsupported kind of term.") in - fun lclrk env -> + fun (ModBodyRK lclrk) env -> (* The order of the declaration matters, for instance (and it's at the time this comment is being written, the only relevent instance) the int31 type registration absolutely needs int31 bits to be registered. |