aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/interface/ascent.mli
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface/ascent.mli')
-rw-r--r--contrib/interface/ascent.mli4
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index dfe64d227..09980413a 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -467,8 +467,8 @@ and ct_MODULE_EXPR =
| CT_module_app of ct_MODULE_EXPR * ct_MODULE_EXPR
and ct_MODULE_TYPE =
CT_coerce_ID_to_MODULE_TYPE of ct_ID
- | CT_module_type_with_def of ct_MODULE_TYPE * ct_ID * ct_FORMULA
- | CT_module_type_with_mod of ct_MODULE_TYPE * ct_ID * ct_ID
+ | CT_module_type_with_def of ct_MODULE_TYPE * ct_ID_LIST * ct_FORMULA
+ | CT_module_type_with_mod of ct_MODULE_TYPE * ct_ID_LIST * ct_ID
and ct_MODULE_TYPE_CHECK =
CT_coerce_MODULE_TYPE_OPT_to_MODULE_TYPE_CHECK of ct_MODULE_TYPE_OPT
| CT_only_check of ct_MODULE_TYPE