diff options
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 63c690d485..475ef042d1 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -251,13 +251,14 @@ type structure_field_body = | SFBconst of constant_body | SFBmind of mutual_inductive_body | SFBmodule of module_body - | SFBmodtype of struct_expr_body + | SFBalias of module_path * constraints option + | SFBmodtype of module_type_body and structure_body = (label * structure_field_body) list and struct_expr_body = | SEBident of module_path - | SEBfunctor of mod_bound_id * struct_expr_body * struct_expr_body + | SEBfunctor of mod_bound_id * module_type_body * struct_expr_body | SEBstruct of mod_self_id * structure_body | SEBapply of struct_expr_body * struct_expr_body * constraints @@ -270,8 +271,11 @@ and with_declaration_body = and module_body = { mod_expr : struct_expr_body option; mod_type : struct_expr_body option; - mod_equiv : module_path option; mod_constraints : constraints; + mod_alias : substitution; mod_retroknowledge : Retroknowledge.action list} -type module_type_body = struct_expr_body * module_path option +and module_type_body = + { typ_expr : struct_expr_body; + typ_strength : module_path option; + typ_alias : substitution} |