diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst
index b45cdfede1949..b742846cebd3c 100644
--- a/doc/sphinx/language/core/modules.rst
+++ b/doc/sphinx/language/core/modules.rst
@@ -171,7 +171,7 @@ are now available through the dot notation.
   #. Assumptions such as :cmd:`Axiom` that include the :n:`Inline` clause will be automatically
      expanded when the functor is applied, except when the function application is prefixed by ``!``.
 
-.. cmd:: Include @module_type_inl {* <+ @module_expr_inl }
+.. cmd:: Include @module_type_inl {* <+ @module_type_inl }
 
    Includes the content of module(s) in the current
    interactive module. Here :n:`@module_type_inl` can be a module expression or a module
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 95d6ed4300d16..3e4a530565463 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1155,7 +1155,7 @@ gallina_ext: [
 | "From" global "Require" export_token LIST1 filtered_import
 | "Import" OPT import_categories LIST1 filtered_import
 | "Export" OPT import_categories LIST1 filtered_import
-| "Include" module_type_inl LIST0 ext_module_expr
+| "Include" module_type_inl LIST0 ext_module_type
 | "Transparent" OPT "!" LIST1 smart_global
 | "Opaque" OPT "!" LIST1 smart_global
 | "Strategy" LIST1 [ strategy_level "[" LIST1 smart_global "]" ]
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 25f2a1393cb74..f8e9bed7a83ba 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -937,7 +937,7 @@ command: [
 | OPT [ "From" dirpath ] "Require" OPT ( [ "Import" | "Export" ] OPT import_categories ) LIST1 filtered_import
 | "Import" OPT import_categories LIST1 filtered_import
 | "Export" OPT import_categories LIST1 filtered_import
-| "Include" module_type_inl LIST0 ( "<+" module_expr_inl )
+| "Include" module_type_inl LIST0 ( "<+" module_type_inl )
 | "Transparent" OPT "!" LIST1 reference
 | "Opaque" OPT "!" LIST1 reference
 | "Strategy" LIST1 [ strategy_level "[" LIST1 reference "]" ]
diff --git a/test-suite/modules/include_module_type.v b/test-suite/modules/include_module_type.v
new file mode 100644
index 0000000000000..bfccfc155a4e0
--- /dev/null
+++ b/test-suite/modules/include_module_type.v
@@ -0,0 +1,14 @@
+Module Type type1.
+  Parameter A : Prop.
+End type1.
+
+Module Type type2.
+  Parameter B : Prop.
+End type2.
+
+Module Type type3 := type1 <+ type2 with Definition B := True.
+Print type3.
+
+Module Type type3''.
+  Include type1 <+ type2 with Definition B := True.
+End type3''.
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index bcf96480ec921..6e565f799c161 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -681,7 +681,7 @@ GRAMMAR EXTEND Gram
         { VernacSynterp (VernacImport ((Import,cats),qidl)) }
       | IDENT "Export"; cats = OPT import_categories; qidl = LIST1 filtered_import ->
         { VernacSynterp (VernacImport ((Export,cats),qidl)) }
-      | IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_expr ->
+      | IDENT "Include"; e = module_type_inl; l = LIST0 ext_module_type ->
           { VernacSynterp (VernacInclude(e::l)) } ] ]
   ;
   import_categories: