From 67cde16ad73ebad8322dcb4d02f3d798de9d28f8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sun, 29 Aug 2021 15:37:45 +0200
Subject: [PATCH] One step further in identifying the syntax of module types
 and module expressions.

---
 vernac/g_vernac.mlg | 31 ++++++++++++-------------------
 1 file changed, 12 insertions(+), 19 deletions(-)

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 5b3b0ef1e144..3d1ff4f5126c 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -620,7 +620,7 @@ GRAMMAR EXTEND Gram
         body = module_body ->
           { VernacSynterp (VernacDeclareModuleType (id, bl, sign, body)) }
       | IDENT "Declare"; IDENT "Module"; export = export_token; id = identref;
-        bl = LIST0 module_binder; ":"; mty = module_type_inl ->
+        bl = LIST0 module_binder; ":"; mty = module_expr_inl ->
           { VernacSynterp (VernacDeclareModule (export, id, bl, mty)) }
       (* Section beginning *)
       | IDENT "Section"; id = identref -> { VernacSynterp (VernacBeginSection id) }
@@ -648,9 +648,9 @@ 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"; l = LIST1 module_type_inl SEP "<+" ->
+      | IDENT "Include"; l = LIST1 module_expr_inl SEP "<+" ->
           { VernacSynterp (VernacInclude l) }
-      | IDENT "Include"; "Type"; l = LIST1 module_type_inl SEP "<+" ->
+      | IDENT "Include"; "Type"; l = LIST1 module_expr_inl SEP "<+" ->
           { warn_deprecated_include_type ~loc ();
             VernacSynterp (VernacInclude l) } ] ]
   ;
@@ -673,17 +673,17 @@ GRAMMAR EXTEND Gram
       |  -> { None } ] ]
   ;
   check_module_type:
-    [ [ "<:"; mty = module_type_inl -> { mty } ] ]
+    [ [ "<:"; mty = module_expr_inl -> { mty } ] ]
   ;
   check_module_types:
     [ [ mtys = LIST0 check_module_type -> { mtys } ] ]
   ;
   of_module_type:
-    [ [ ":"; mty = module_type_inl -> { Enforce mty }
+    [ [ ":"; mty = module_expr_inl -> { Enforce mty }
       | mtys = check_module_types -> { Check mtys } ] ]
   ;
   module_body:
-    [ [ ":="; l = LIST1 module_type_inl SEP "<+" -> { l }
+    [ [ ":="; l = LIST1 module_expr_inl SEP "<+" -> { l }
       | -> { [] } ] ]
   ;
   functor_app_annot:
@@ -693,19 +693,21 @@ GRAMMAR EXTEND Gram
       | -> { DefaultInline }
       ] ]
   ;
-  module_type_inl:
-    [ [ "!"; me = module_type -> { (me,NoInline) }
-      | me = module_type; a = functor_app_annot -> { (me,a) } ] ]
+  module_expr_inl:
+    [ [ "!"; me = module_expr -> { (me,NoInline) }
+      | me = module_expr; a = functor_app_annot -> { (me,a) } ] ]
   ;
   (* Module binder  *)
   module_binder:
     [ [ "("; export = export_token; idl = LIST1 identref; ":";
-         mty = module_type_inl; ")" -> { (export,idl,mty) } ] ]
+         mty = module_expr_inl; ")" -> { (export,idl,mty) } ] ]
   ;
   (* Module expressions *)
   module_expr:
     [ [ me = module_expr_atom -> { CAst.make ~loc @@ CMident me }
       | me1 = module_expr; me2 = module_expr_atom -> { CAst.make ~loc @@ CMapply (me1,me2) }
+      | me = module_expr; "with"; decl = with_declaration ->
+          { CAst.make ~loc @@ CMwith (me,decl) }
       ] ]
   ;
   module_expr_atom:
@@ -718,15 +720,6 @@ GRAMMAR EXTEND Gram
           { CWith_Module (fqid,qid) }
       ] ]
   ;
-  module_type:
-    [ [ qid = qualid -> { CAst.make ~loc @@ CMident qid }
-      | "("; mt = module_type; ")" -> { mt }
-      | mty = module_type; me = module_expr_atom ->
-          { CAst.make ~loc @@ CMapply (mty,me) }
-      | mty = module_type; "with"; decl = with_declaration ->
-          { CAst.make ~loc @@ CMwith (mty,decl) }
-      ] ]
-  ;
   (* Proof using *)
   section_subset_expr:
     [ [ test_only_starredidentrefs; l = LIST0 starredidentref ->