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 /API | |
| parent | 1974816aca996fe3ee9420b83f11d15923e70fda (diff) | |
Statically enforcing that module types have no retroknowledge.
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/API/API.mli b/API/API.mli index aa7f93bb25..2a60cd54a9 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1287,7 +1287,7 @@ sig mod_type_alg : module_expression option; mod_constraints : Univ.ContextSet.t; mod_delta : Mod_subst.delta_resolver; - mod_retroknowledge : Retroknowledge.action list + mod_retroknowledge : 'a module_retroknowledge; } and module_signature = (module_type_body,structure_body) functorize and module_body = module_implementation generic_module_body @@ -1298,6 +1298,10 @@ sig | SFBmind of mutual_inductive_body | SFBmodule of module_body | SFBmodtype of module_type_body + and _ module_retroknowledge = + | ModBodyRK : + Retroknowledge.action list -> module_implementation module_retroknowledge + | ModTypeRK : unit module_retroknowledge end module Declareops : |