diff options
Diffstat (limited to 'kernel/entries.ml')
| -rw-r--r-- | kernel/entries.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/entries.ml b/kernel/entries.ml index 504c11fdfb..6ea4bfc591 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -85,8 +85,8 @@ and module_type_entry = and module_signature_entry = (label * specification_entry) list and with_declaration = - With_Module of identifier * module_path - | With_Definition of identifier * constr + With_Module of identifier list * module_path + | With_Definition of identifier list * constr and module_expr = MEident of module_path |