aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/topconstr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'interp/topconstr.mli')
-rw-r--r--interp/topconstr.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 1966bf552..1b6514a65 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -256,8 +256,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
val ntn_loc : Util.loc -> constr_expr notation_substitution -> string -> int
val patntn_loc : Util.loc -> cases_pattern_expr notation_substitution -> string -> int