diff options
Diffstat (limited to 'plugins/interface/ascent.mli')
| -rw-r--r-- | plugins/interface/ascent.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/interface/ascent.mli b/plugins/interface/ascent.mli index bc615f14ec..bd82688d33 100644 --- a/plugins/interface/ascent.mli +++ b/plugins/interface/ascent.mli @@ -479,7 +479,7 @@ and ct_MODULE_TYPE = | 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 + | CT_only_check of ct_MODULE_TYPE list and ct_MODULE_TYPE_OPT = CT_coerce_ID_OPT_to_MODULE_TYPE_OPT of ct_ID_OPT | CT_coerce_MODULE_TYPE_to_MODULE_TYPE_OPT of ct_MODULE_TYPE |