diff options
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 475ef042d1..725859321c 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -251,7 +251,8 @@ type structure_field_body = | SFBconst of constant_body | SFBmind of mutual_inductive_body | SFBmodule of module_body - | SFBalias of module_path * constraints option + | SFBalias of module_path * struct_expr_body option + * constraints option | SFBmodtype of module_type_body and structure_body = (label * structure_field_body) list @@ -265,7 +266,8 @@ and struct_expr_body = | SEBwith of struct_expr_body * with_declaration_body and with_declaration_body = - With_module_body of identifier list * module_path * constraints + With_module_body of identifier list * module_path + * struct_expr_body option * constraints | With_definition_body of identifier list * constant_body and module_body = |