aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/topconstr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/topconstr.ml')
-rw-r--r--interp/topconstr.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index df48458e6..12ce52d1b 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -1012,8 +1012,8 @@ type module_type_ast =
| CMTEwith of module_type_ast * with_declaration_ast
type include_ast =
- | CIMTE of module_type_ast
- | CIME of module_ast
+ | CIMTE of module_type_ast * module_type_ast list
+ | CIME of module_ast * module_ast list
let loc_of_notation f loc (args,_) ntn =
if args=[] or ntn.[0] <> '_' then fst (Util.unloc loc)