aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/vernacexpr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/vernacexpr.ml')
-rw-r--r--toplevel/vernacexpr.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 366308bfa..ccb850651 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -261,9 +261,9 @@ type vernac_expr =
| VernacDeclareModule of bool option * lident *
module_binder list * (module_type_ast * bool)
| VernacDefineModule of bool option * lident *
- module_binder list * (module_type_ast * bool) option * module_ast option
+ module_binder list * (module_type_ast * bool) option * module_ast list
| VernacDeclareModuleType of lident *
- module_binder list * module_type_ast option
+ module_binder list * module_type_ast list
| VernacInclude of bool * include_ast
(* Solving *)