Support Include Module Type with

Villetaneuse · May 16, 2024 · d68020b · d68020b
1 parent 886e8b5
commit d68020b
Show file tree

Hide file tree

Showing 5 changed files with 18 additions and 4 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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: