aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/topconstr.ml4
-rw-r--r--interp/topconstr.mli4
2 files changed, 4 insertions, 4 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index ecb61e15b0..3d2e3fde0d 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -1024,8 +1024,8 @@ type module_type_ast =
| CMTEwith of module_type_ast * with_declaration_ast
type include_ast =
- | CIMTE of module_type_ast * module_type_ast list
- | CIME of module_ast * module_ast list
+ | CIMTE of module_type_ast list
+ | CIME of module_ast list
type 'a module_signature =
| Enforce of 'a (* ... : T *)
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index b7e389d6b3..36f8cfad39 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -257,8 +257,8 @@ type module_type_ast =
| CMTEwith of module_type_ast * with_declaration_ast
type include_ast =
- | CIMTE of module_type_ast * module_type_ast list
- | CIME of module_ast * module_ast list
+ | CIMTE of module_type_ast list
+ | CIME of module_ast list
type 'a module_signature =
| Enforce of 'a (* ... : T *)