diff options
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 1b32d343ee..e17fb1c38f 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 |