Merge PR coq#19144: Include module type with definition

Reviewed-by: proux01 Co-authored-by: proux01 <[email protected]>
SkySkimmer · Jun 9, 2024 · 054e150 · 054e150
2 parents 526a447 + ac79ea4
commit 054e150
Show file tree

Hide file tree

Showing 6 changed files with 23 additions and 4 deletions.
diff --git a/...og/08-vernac-commands-and-options/19144-include-module-type-with-definition.rst b/...og/08-vernac-commands-and-options/19144-include-module-type-with-definition.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+  The :cmd:`Include` command can now include module types with a `with` clause (:n:`@with_declaration`)
+  to instantiate some parameters
+  (`#19144 <https://github.com/coq/coq/pull/19144>`_,
+  by Pierre Rousselin).
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
@@ -1156,7 +1156,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
 | "Include" "Type" module_type_inl LIST0 ext_module_type
 | "Transparent" OPT "!" LIST1 smart_global
 | "Opaque" OPT "!" LIST1 smart_global

diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
@@ -938,7 +938,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 )
 | "Include" "Type" LIST1 module_type_inl SEP "<+"
 | "Transparent" OPT "!" LIST1 reference
 | "Opaque" OPT "!" 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
@@ -689,7 +689,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)) }
       | IDENT "Include"; "Type"; e = module_type_inl; l = LIST0 ext_module_type ->
          { warn_deprecated_include_type ~loc ();