diff options
Diffstat (limited to 'kernel/declarations.mli')
| -rw-r--r-- | kernel/declarations.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/declarations.mli b/kernel/declarations.mli index 7f7f7dcc39..2f32d86392 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -218,7 +218,8 @@ 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} (* [type_of(mod_expr)] <: [mod_user_type] (if given) *) (* if equiv given then constraints are empty *) |