aboutsummaryrefslogtreecommitdiff
path: root/contrib/interface/vtp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface/vtp.ml')
-rw-r--r--contrib/interface/vtp.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index ebad140808..ff67c14859 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -1157,12 +1157,12 @@ and fMODULE_TYPE = function
| CT_coerce_ID_to_MODULE_TYPE x -> fID x
| CT_module_type_with_def(x1, x2, x3) ->
fMODULE_TYPE x1;
- fID x2;
+ fID_LIST x2;
fFORMULA x3;
fNODE "module_type_with_def" 3
| CT_module_type_with_mod(x1, x2, x3) ->
fMODULE_TYPE x1;
- fID x2;
+ fID_LIST x2;
fID x3;
fNODE "module_type_with_mod" 3
and fMODULE_TYPE_CHECK = function