diff options
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 1be251a503..eb49ba6203 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -285,5 +285,6 @@ and module_body = mod_user_type : module_type_body option; mod_type : module_type_body; mod_equiv : module_path option; - mod_constraints : constraints } + mod_constraints : constraints; + mod_retroknowledge : Retroknowledge.action list} |