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/declarations.ml | |
| parent | 1974816aca996fe3ee9420b83f11d15923e70fda (diff) | |
Statically enforcing that module types have no retroknowledge.
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 1b32d343e..e17fb1c38 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -259,7 +259,7 @@ and 'a generic_module_body = set of all universes constraints in the module *) mod_delta : Mod_subst.delta_resolver; (** quotiented set of equivalent constants and inductive names *) - mod_retroknowledge : Retroknowledge.action list } + mod_retroknowledge : 'a module_retroknowledge } (** For a module, there are five possible situations: - [Declare Module M : T] then [mod_expr = Abstract; mod_type_alg = Some T] @@ -278,6 +278,11 @@ and module_body = module_implementation generic_module_body and module_type_body = unit generic_module_body +and _ module_retroknowledge = +| ModBodyRK : + Retroknowledge.action list -> module_implementation module_retroknowledge +| ModTypeRK : unit module_retroknowledge + (** Extra invariants : - No [MEwith] inside a [mod_expr] implementation : the 'with' syntax |