diff --git a/document/core/binary/modules.rst b/document/core/binary/modules.rst
index ccb7b5fe3..f9315162c 100644
--- a/document/core/binary/modules.rst
+++ b/document/core/binary/modules.rst
@@ -138,7 +138,7 @@ $${grammar: {Btypesec Btype}}
 .. index:: ! import section, import, name, function type, table type, memory type, global type, tag type
    pair: binary format; import
    pair: section; import
-.. _binary-import:
+.. _binary-importitem:
 .. _binary-imports:
 .. _binary-importdesc:
 .. _binary-importsec:
@@ -149,10 +149,10 @@ Import Section
 The *import section* has the id 2.
 It decodes into the list of :ref:`imports <syntax-import>` of a :ref:`module <syntax-module>`.
 
-$${grammar: {Bimportsec Bimports Bimport}}
+$${grammar: {Bimportsec Bimports Bimportitem}}
 
 .. note::
-   The encoding of :ref:`imports <binary-imports>` containing ${:0x7F} allows multiple imports to be encoded without repeating the module name. Because ${:0x7F} is not a valid encoding for an :ref:`external type <binary-externtype>`, the encoding is unambiguous.
+   The encodings of :ref:`imports <binary-imports>` containing ${:0x7F} and ${:0x7E} allow multiple imports to be encoded without repeating the module name, and potentially also without repeating the externtype. Because ${:0x7F} and ${:0x7E} are not valid encodings for an :ref:`external type <binary-externtype>`, the encoding is unambiguous.
 
 
 .. index:: ! function section, function, type index, function type
diff --git a/document/core/text/modules.rst b/document/core/text/modules.rst
index f222e83f9..7b392e4db 100644
--- a/document/core/text/modules.rst
+++ b/document/core/text/modules.rst
@@ -357,9 +357,13 @@ $${grammar: Timport_/plain}
 Abbreviations
 .............
 
-Multiple imports with the same ${:nm_1} may be declared together:
+Multiple imports with the same :ref:`name <syntax-name>` ${:nm_1} may be declared together:
 
-$${grammar: Timports_/abbrev}
+$${grammar: Timports_/abbrev-compact1}
+
+Multiple imports with the same :ref:`name <syntax-name>` ${:nm_1} and :ref:`external type <syntax-externtype>` may also be declared together:
+
+$${grammar: Timports_/abbrev-compact2}
 
 Imports may also be specified inline with
 :ref:`tag <text-tag>`,
diff --git a/document/core/util/macros.def b/document/core/util/macros.def
index 4a2ef3e41..783480c62 100644
--- a/document/core/util/macros.def
+++ b/document/core/util/macros.def
@@ -886,7 +886,7 @@
 .. |Bmem| mathdef:: \xref{binary/modules}{binary-mem}{\B{mem}}
 .. |Bglobal| mathdef:: \xref{binary/modules}{binary-global}{\B{global}}
 .. |Btag| mathdef:: \xref{binary/modules}{binary-tag}{\B{tag}}
-.. |Bimport| mathdef:: \xref{binary/modules}{binary-import}{\B{import}}
+.. |Bimportitem| mathdef:: \xref{binary/modules}{binary-importitem}{\B{importitem}}
 .. |Bimports| mathdef:: \xref{binary/modules}{binary-imports}{\B{imports}}
 .. |Bexport| mathdef:: \xref{binary/modules}{binary-export}{\B{export}}
 .. |Belem| mathdef:: \xref{binary/modules}{binary-elem}{\B{elem}}
diff --git a/specification/wasm-3.0/5.4-binary.modules.spectec b/specification/wasm-3.0/5.4-binary.modules.spectec
index 8bf570f8e..63476f29a 100644
--- a/specification/wasm-3.0/5.4-binary.modules.spectec
+++ b/specification/wasm-3.0/5.4-binary.modules.spectec
@@ -31,12 +31,13 @@ grammar Btypesec : type* hint(desc "type section") =
 
 ;; Import section
 
-grammar Bimport : (name, externtype) =
+grammar Bimportitem : (name, externtype) =
   | nm_2:Bname xt:Bexterntype => (nm_2, xt)
 
 grammar Bimports : import* =
-  | nm_1:Bname (nm_2, xt):Bimport => IMPORT nm_1 nm_2 xt
-  | nm_1:Bname nm_e:Bname 0x7F (nm_2, xt)*:Blist(Bimport) => (IMPORT nm_1 nm_2 xt)*  -- if nm_e = eps
+  | nm_1:Bname nm_2:Bname xt:Bexterntype => IMPORT nm_1 nm_2 xt
+  | nm_1:Bname nm_e:Bname 0x7F (nm_2, xt)*:Blist(Bimportitem) => (IMPORT nm_1 nm_2 xt)*  -- if nm_e = eps
+  | nm_1:Bname nm_e:Bname 0x7E xt:Bexterntype nm_2*:Blist(Bname) => (IMPORT nm_1 nm_2 xt)*  -- if nm_e = eps
 
 grammar Bimportsec : import* hint(desc "import section") =
   | im**:Bsection_(2, Blist(Bimports)) => $concat_(import, im**)
diff --git a/specification/wasm-3.0/6.3-text.modules.spectec b/specification/wasm-3.0/6.3-text.modules.spectec
index 7cee6a76a..5468664e4 100644
--- a/specification/wasm-3.0/6.3-text.modules.spectec
+++ b/specification/wasm-3.0/6.3-text.modules.spectec
@@ -134,9 +134,14 @@ grammar Timport_(I)/plain : (import, idctxt) =
   | "(" "import" nm_1:Tname nm_2:Tname (xt,I'):Texterntype_(I) ")" => (IMPORT nm_1 nm_2 xt, I')
   | ...
 
-grammar Timports_(I)/abbrev : (import*, idctxt) =
+grammar Timports_(I)/abbrev-compact1 : (import*, idctxt) =
   | "(" "import" nm_1:Tname ("(" "item" nm_2:Tname Texterntype_(I) ")")* ")" ==
     ("(" "import" nm_1:Tname nm_2:Tname Texterntype_(I) ")")*
+  | ...
+
+grammar Timports_(I)/abbrev-compact2 : (import*, idctxt) = ...
+  | "(" "import" nm_1:Tname ("(" "item" nm_2:Tname ")")* Texterntype_(I) ")" ==
+    ("(" "import" nm_1:Tname nm_2:Tname Texterntype_(I) ")")*
 
 grammar Timport_(I)/abbrev-tag : (import, idctxt) = ...
   | "(" "tag" Tid? "(" "import" Tname^2 ")" Ttagtype_(I) ")" ==
diff --git a/spectec/doc/example/output/NanoWasm.pdf b/spectec/doc/example/output/NanoWasm.pdf
index cfd46145b..7791fea59 100644
Binary files a/spectec/doc/example/output/NanoWasm.pdf and b/spectec/doc/example/output/NanoWasm.pdf differ
diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md
index 03e2f9250..566ec7607 100644
--- a/spectec/test-frontend/TEST.md
+++ b/spectec/test-frontend/TEST.md
@@ -8708,16 +8708,19 @@ grammar Btypesec : type*
   prod{`ty*` : type*} ty*{ty <- `ty*`}:Bsection_(1, syntax type, grammar Blist(syntax type, grammar Btype)) => ty*{ty <- `ty*`}
 
 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
-grammar Bimport : (name, externtype)
+grammar Bimportitem : (name, externtype)
   ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
   prod{nm_2 : name, xt : externtype} {{nm_2:Bname} {xt:Bexterntype}} => (nm_2, xt)
 
 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
 grammar Bimports : import*
   ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
-  prod{nm_1 : name, nm_2 : name, xt : externtype} {{nm_1:Bname} {(nm_2, xt):Bimport}} => [IMPORT_import(nm_1, nm_2, xt)]
+  prod{nm_1 : name, nm_2 : name, xt : externtype} {{nm_1:Bname} {nm_2:Bname} {xt:Bexterntype}} => [IMPORT_import(nm_1, nm_2, xt)]
   ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
-  prod{nm_1 : name, nm_e : name, `nm_2*` : name*, `xt*` : externtype*} {{nm_1:Bname} {nm_e:Bname} {0x7F} {(nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}:Blist(syntax (name, externtype), grammar Bimport)}} => IMPORT_import(nm_1, nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}
+  prod{nm_1 : name, nm_e : name, `nm_2*` : name*, `xt*` : externtype*} {{nm_1:Bname} {nm_e:Bname} {0x7F} {(nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}:Blist(syntax (name, externtype), grammar Bimportitem)}} => IMPORT_import(nm_1, nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}
+    -- if (nm_e = `%`_name([]))
+  ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
+  prod{nm_1 : name, nm_e : name, xt : externtype, `nm_2*` : name*} {{nm_1:Bname} {nm_e:Bname} {0x7E} {xt:Bexterntype} {nm_2*{nm_2 <- `nm_2*`}:Blist(syntax name, grammar Bname)}} => IMPORT_import(nm_1, nm_2, xt)*{nm_2 <- `nm_2*`}
     -- if (nm_e = `%`_name([]))
 
 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
@@ -10974,13 +10977,13 @@ syntax decl =
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:261.1-261.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:266.1-266.76
 def $typesd(decl*) : type*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:273.1-273.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:278.1-278.23
   def $typesd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:274.1-274.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:279.1-279.48
   def $typesd{type : type, `decl'*` : decl*}([(type : type <: decl)] ++ decl'*{decl' <- `decl'*`}) = [type] ++ $typesd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:275.1-275.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:280.1-280.57
   def $typesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $typesd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -10988,13 +10991,13 @@ def $typesd(decl*) : type*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:262.1-262.78
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:267.1-267.78
 def $importsd(decl*) : import*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:277.1-277.25
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:282.1-282.25
   def $importsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:278.1-278.56
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:283.1-283.56
   def $importsd{import : import, `decl'*` : decl*}([(import : import <: decl)] ++ decl'*{decl' <- `decl'*`}) = [import] ++ $importsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:279.1-279.61
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:284.1-284.61
   def $importsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $importsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11002,13 +11005,13 @@ def $importsd(decl*) : import*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:263.1-263.75
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:268.1-268.75
 def $tagsd(decl*) : tag*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:281.1-281.22
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:286.1-286.22
   def $tagsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:282.1-282.44
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:287.1-287.44
   def $tagsd{tag : tag, `decl'*` : decl*}([(tag : tag <: decl)] ++ decl'*{decl' <- `decl'*`}) = [tag] ++ $tagsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:283.1-283.55
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:288.1-288.55
   def $tagsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tagsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11016,13 +11019,13 @@ def $tagsd(decl*) : tag*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:264.1-264.78
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:269.1-269.78
 def $globalsd(decl*) : global*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:285.1-285.25
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:290.1-290.25
   def $globalsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:286.1-286.56
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:291.1-291.56
   def $globalsd{global : global, `decl'*` : decl*}([(global : global <: decl)] ++ decl'*{decl' <- `decl'*`}) = [global] ++ $globalsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:287.1-287.61
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:292.1-292.61
   def $globalsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $globalsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11030,13 +11033,13 @@ def $globalsd(decl*) : global*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:265.1-265.75
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:270.1-270.75
 def $memsd(decl*) : mem*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:289.1-289.22
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:294.1-294.22
   def $memsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:290.1-290.44
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:295.1-295.44
   def $memsd{mem : mem, `decl'*` : decl*}([(mem : mem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [mem] ++ $memsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:291.1-291.55
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:296.1-296.55
   def $memsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $memsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11044,13 +11047,13 @@ def $memsd(decl*) : mem*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:266.1-266.77
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:271.1-271.77
 def $tablesd(decl*) : table*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:293.1-293.24
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:298.1-298.24
   def $tablesd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:294.1-294.52
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:299.1-299.52
   def $tablesd{table : table, `decl'*` : decl*}([(table : table <: decl)] ++ decl'*{decl' <- `decl'*`}) = [table] ++ $tablesd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:295.1-295.59
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:300.1-300.59
   def $tablesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tablesd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11058,13 +11061,13 @@ def $tablesd(decl*) : table*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:267.1-267.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:272.1-272.76
 def $funcsd(decl*) : func*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:297.1-297.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:302.1-302.23
   def $funcsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:298.1-298.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:303.1-303.48
   def $funcsd{func : func, `decl'*` : decl*}([(func : func <: decl)] ++ decl'*{decl' <- `decl'*`}) = [func] ++ $funcsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:299.1-299.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:304.1-304.57
   def $funcsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $funcsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11072,13 +11075,13 @@ def $funcsd(decl*) : func*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:268.1-268.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:273.1-273.76
 def $datasd(decl*) : data*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:301.1-301.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:306.1-306.23
   def $datasd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:302.1-302.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:307.1-307.48
   def $datasd{data : data, `decl'*` : decl*}([(data : data <: decl)] ++ decl'*{decl' <- `decl'*`}) = [data] ++ $datasd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:303.1-303.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:308.1-308.57
   def $datasd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $datasd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11086,13 +11089,13 @@ def $datasd(decl*) : data*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:269.1-269.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:274.1-274.76
 def $elemsd(decl*) : elem*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:305.1-305.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:310.1-310.23
   def $elemsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:306.1-306.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:311.1-311.48
   def $elemsd{elem : elem, `decl'*` : decl*}([(elem : elem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [elem] ++ $elemsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:307.1-307.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:312.1-312.57
   def $elemsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $elemsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11100,13 +11103,13 @@ def $elemsd(decl*) : elem*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:270.1-270.77
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:275.1-275.77
 def $startsd(decl*) : start*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:309.1-309.24
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:314.1-314.24
   def $startsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:310.1-310.52
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:315.1-315.52
   def $startsd{start : start, `decl'*` : decl*}([(start : start <: decl)] ++ decl'*{decl' <- `decl'*`}) = [start] ++ $startsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:311.1-311.59
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:316.1-316.59
   def $startsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $startsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11114,13 +11117,13 @@ def $startsd(decl*) : start*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:271.1-271.78
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:276.1-276.78
 def $exportsd(decl*) : export*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:313.1-313.25
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:318.1-318.25
   def $exportsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:314.1-314.56
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:319.1-319.56
   def $exportsd{export : export, `decl'*` : decl*}([(export : export <: decl)] ++ decl'*{decl' <- `decl'*`}) = [export] ++ $exportsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:315.1-315.61
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:320.1-320.61
   def $exportsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $exportsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md
index 9cab84c70..3e90d188c 100644
--- a/spectec/test-latex/TEST.md
+++ b/spectec/test-latex/TEST.md
@@ -12024,9 +12024,10 @@ $$
 
 $$
 \begin{array}[t]{@{}lrrl@{}l@{}l@{}l@{}}
-& {\mathtt{import}} & ::= & {\mathit{nm}}_2{:}{\mathtt{name}}~~{\mathit{xt}}{:}{\mathtt{externtype}} & \quad\Rightarrow\quad{} & ({\mathit{nm}}_2, {\mathit{xt}}) \\
-& {\mathtt{imports}} & ::= & {\mathit{nm}}_1{:}{\mathtt{name}}~~({\mathit{nm}}_2, {\mathit{xt}}){:}{\mathtt{import}} & \quad\Rightarrow\quad{} & \mathsf{import}~{\mathit{nm}}_1~{\mathit{nm}}_2~{\mathit{xt}} \\
-& & | & {\mathit{nm}}_1{:}{\mathtt{name}}~~{\mathit{nm}}_e{:}{\mathtt{name}}~~\mathtt{0x7F}~~{({\mathit{nm}}_2, {\mathit{xt}})^\ast}{:}{\mathtt{list}}({\mathtt{import}}) & \quad\Rightarrow\quad{} & {(\mathsf{import}~{\mathit{nm}}_1~{\mathit{nm}}_2~{\mathit{xt}})^\ast} & \quad \mbox{if}~ {\mathit{nm}}_e = \epsilon \\
+& {\mathtt{importitem}} & ::= & {\mathit{nm}}_2{:}{\mathtt{name}}~~{\mathit{xt}}{:}{\mathtt{externtype}} & \quad\Rightarrow\quad{} & ({\mathit{nm}}_2, {\mathit{xt}}) \\
+& {\mathtt{imports}} & ::= & {\mathit{nm}}_1{:}{\mathtt{name}}~~{\mathit{nm}}_2{:}{\mathtt{name}}~~{\mathit{xt}}{:}{\mathtt{externtype}} & \quad\Rightarrow\quad{} & \mathsf{import}~{\mathit{nm}}_1~{\mathit{nm}}_2~{\mathit{xt}} \\
+& & | & {\mathit{nm}}_1{:}{\mathtt{name}}~~{\mathit{nm}}_e{:}{\mathtt{name}}~~\mathtt{0x7F}~~{({\mathit{nm}}_2, {\mathit{xt}})^\ast}{:}{\mathtt{list}}({\mathtt{importitem}}) & \quad\Rightarrow\quad{} & {(\mathsf{import}~{\mathit{nm}}_1~{\mathit{nm}}_2~{\mathit{xt}})^\ast} & \quad \mbox{if}~ {\mathit{nm}}_e = \epsilon \\
+& & | & {\mathit{nm}}_1{:}{\mathtt{name}}~~{\mathit{nm}}_e{:}{\mathtt{name}}~~\mathtt{0x7E}~~{\mathit{xt}}{:}{\mathtt{externtype}}~~{{\mathit{nm}}_2^\ast}{:}{\mathtt{list}}({\mathtt{name}}) & \quad\Rightarrow\quad{} & {(\mathsf{import}~{\mathit{nm}}_1~{\mathit{nm}}_2~{\mathit{xt}})^\ast} & \quad \mbox{if}~ {\mathit{nm}}_e = \epsilon \\
 \mbox{(import section)} & {\mathtt{importsec}} & ::= & {{{\mathit{im}}^\ast}^\ast}{:}{{\mathtt{section}}}_{2}({\mathtt{list}}({\mathtt{imports}})) & \quad\Rightarrow\quad{} & {\bigoplus}\, {{{\mathit{im}}^\ast}^\ast} \\
 \end{array}
 $$
@@ -13589,6 +13590,12 @@ $$
 {(\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{import}’}~~{\mathit{nm}}_1{:}{\mathtt{name}}~~{\mathit{nm}}_2{:}{\mathtt{name}}~~{{\mathtt{externtype}}}_{I}~~\mbox{‘\texttt{{)}}’})^\ast} \\
 \end{array}
 } \\
+& & | & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{import}’}~~{\mathit{nm}}_1{:}{\mathtt{name}}~~{(\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{item}’}~~{\mathit{nm}}_2{:}{\mathtt{name}}~~\mbox{‘\texttt{{)}}’})^\ast}~~{{\mathtt{externtype}}}_{I}~~\mbox{‘\texttt{{)}}’} & \quad\equiv\quad{} & & \\
+&&& \multicolumn{4}{@{}l@{}}{\quad
+\begin{array}[t]{@{}l@{}}
+{(\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{import}’}~~{\mathit{nm}}_1{:}{\mathtt{name}}~~{\mathit{nm}}_2{:}{\mathtt{name}}~~{{\mathtt{externtype}}}_{I}~~\mbox{‘\texttt{{)}}’})^\ast} \\
+\end{array}
+} \\
 & {{\mathtt{import}}}_{I} & ::= & \dots \\
 & & | & \mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{tag}’}~~{{\mathtt{id}}^?}~~\mbox{‘\texttt{{(}}’}~~\mbox{‘\texttt{import}’}~~{{\mathtt{name}}^{2}}~~\mbox{‘\texttt{{)}}’}~~{{\mathtt{tagtype}}}_{I}~~\mbox{‘\texttt{{)}}’} & \quad\equiv\quad{} & & \\
 &&& \multicolumn{4}{@{}l@{}}{\quad
diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md
index 157523b22..0d20910d9 100644
--- a/spectec/test-middlend/TEST.md
+++ b/spectec/test-middlend/TEST.md
@@ -8698,16 +8698,19 @@ grammar Btypesec : type*
   prod{`ty*` : type*} ty*{ty <- `ty*`}:Bsection_(1, syntax type, grammar Blist(syntax type, grammar Btype)) => ty*{ty <- `ty*`}
 
 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
-grammar Bimport : (name, externtype)
+grammar Bimportitem : (name, externtype)
   ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
   prod{nm_2 : name, xt : externtype} {{nm_2:Bname} {xt:Bexterntype}} => (nm_2, xt)
 
 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
 grammar Bimports : import*
   ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
-  prod{nm_1 : name, nm_2 : name, xt : externtype} {{nm_1:Bname} {(nm_2, xt):Bimport}} => [IMPORT_import(nm_1, nm_2, xt)]
+  prod{nm_1 : name, nm_2 : name, xt : externtype} {{nm_1:Bname} {nm_2:Bname} {xt:Bexterntype}} => [IMPORT_import(nm_1, nm_2, xt)]
   ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
-  prod{nm_1 : name, nm_e : name, `nm_2*` : name*, `xt*` : externtype*} {{nm_1:Bname} {nm_e:Bname} {0x7F} {(nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}:Blist(syntax (name, externtype), grammar Bimport)}} => IMPORT_import(nm_1, nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}
+  prod{nm_1 : name, nm_e : name, `nm_2*` : name*, `xt*` : externtype*} {{nm_1:Bname} {nm_e:Bname} {0x7F} {(nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}:Blist(syntax (name, externtype), grammar Bimportitem)}} => IMPORT_import(nm_1, nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}
+    -- if (nm_e = `%`_name([]))
+  ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
+  prod{nm_1 : name, nm_e : name, xt : externtype, `nm_2*` : name*} {{nm_1:Bname} {nm_e:Bname} {0x7E} {xt:Bexterntype} {nm_2*{nm_2 <- `nm_2*`}:Blist(syntax name, grammar Bname)}} => IMPORT_import(nm_1, nm_2, xt)*{nm_2 <- `nm_2*`}
     -- if (nm_e = `%`_name([]))
 
 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
@@ -10964,13 +10967,13 @@ syntax decl =
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:261.1-261.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:266.1-266.76
 def $typesd(decl*) : type*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:273.1-273.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:278.1-278.23
   def $typesd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:274.1-274.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:279.1-279.48
   def $typesd{type : type, `decl'*` : decl*}([(type : type <: decl)] ++ decl'*{decl' <- `decl'*`}) = [type] ++ $typesd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:275.1-275.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:280.1-280.57
   def $typesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $typesd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -10978,13 +10981,13 @@ def $typesd(decl*) : type*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:262.1-262.78
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:267.1-267.78
 def $importsd(decl*) : import*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:277.1-277.25
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:282.1-282.25
   def $importsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:278.1-278.56
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:283.1-283.56
   def $importsd{import : import, `decl'*` : decl*}([(import : import <: decl)] ++ decl'*{decl' <- `decl'*`}) = [import] ++ $importsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:279.1-279.61
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:284.1-284.61
   def $importsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $importsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -10992,13 +10995,13 @@ def $importsd(decl*) : import*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:263.1-263.75
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:268.1-268.75
 def $tagsd(decl*) : tag*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:281.1-281.22
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:286.1-286.22
   def $tagsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:282.1-282.44
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:287.1-287.44
   def $tagsd{tag : tag, `decl'*` : decl*}([(tag : tag <: decl)] ++ decl'*{decl' <- `decl'*`}) = [tag] ++ $tagsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:283.1-283.55
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:288.1-288.55
   def $tagsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tagsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11006,13 +11009,13 @@ def $tagsd(decl*) : tag*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:264.1-264.78
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:269.1-269.78
 def $globalsd(decl*) : global*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:285.1-285.25
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:290.1-290.25
   def $globalsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:286.1-286.56
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:291.1-291.56
   def $globalsd{global : global, `decl'*` : decl*}([(global : global <: decl)] ++ decl'*{decl' <- `decl'*`}) = [global] ++ $globalsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:287.1-287.61
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:292.1-292.61
   def $globalsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $globalsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11020,13 +11023,13 @@ def $globalsd(decl*) : global*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:265.1-265.75
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:270.1-270.75
 def $memsd(decl*) : mem*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:289.1-289.22
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:294.1-294.22
   def $memsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:290.1-290.44
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:295.1-295.44
   def $memsd{mem : mem, `decl'*` : decl*}([(mem : mem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [mem] ++ $memsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:291.1-291.55
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:296.1-296.55
   def $memsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $memsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11034,13 +11037,13 @@ def $memsd(decl*) : mem*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:266.1-266.77
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:271.1-271.77
 def $tablesd(decl*) : table*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:293.1-293.24
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:298.1-298.24
   def $tablesd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:294.1-294.52
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:299.1-299.52
   def $tablesd{table : table, `decl'*` : decl*}([(table : table <: decl)] ++ decl'*{decl' <- `decl'*`}) = [table] ++ $tablesd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:295.1-295.59
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:300.1-300.59
   def $tablesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tablesd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11048,13 +11051,13 @@ def $tablesd(decl*) : table*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:267.1-267.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:272.1-272.76
 def $funcsd(decl*) : func*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:297.1-297.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:302.1-302.23
   def $funcsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:298.1-298.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:303.1-303.48
   def $funcsd{func : func, `decl'*` : decl*}([(func : func <: decl)] ++ decl'*{decl' <- `decl'*`}) = [func] ++ $funcsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:299.1-299.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:304.1-304.57
   def $funcsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $funcsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11062,13 +11065,13 @@ def $funcsd(decl*) : func*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:268.1-268.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:273.1-273.76
 def $datasd(decl*) : data*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:301.1-301.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:306.1-306.23
   def $datasd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:302.1-302.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:307.1-307.48
   def $datasd{data : data, `decl'*` : decl*}([(data : data <: decl)] ++ decl'*{decl' <- `decl'*`}) = [data] ++ $datasd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:303.1-303.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:308.1-308.57
   def $datasd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $datasd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11076,13 +11079,13 @@ def $datasd(decl*) : data*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:269.1-269.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:274.1-274.76
 def $elemsd(decl*) : elem*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:305.1-305.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:310.1-310.23
   def $elemsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:306.1-306.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:311.1-311.48
   def $elemsd{elem : elem, `decl'*` : decl*}([(elem : elem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [elem] ++ $elemsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:307.1-307.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:312.1-312.57
   def $elemsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $elemsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11090,13 +11093,13 @@ def $elemsd(decl*) : elem*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:270.1-270.77
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:275.1-275.77
 def $startsd(decl*) : start*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:309.1-309.24
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:314.1-314.24
   def $startsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:310.1-310.52
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:315.1-315.52
   def $startsd{start : start, `decl'*` : decl*}([(start : start <: decl)] ++ decl'*{decl' <- `decl'*`}) = [start] ++ $startsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:311.1-311.59
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:316.1-316.59
   def $startsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $startsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -11104,13 +11107,13 @@ def $startsd(decl*) : start*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:271.1-271.78
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:276.1-276.78
 def $exportsd(decl*) : export*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:313.1-313.25
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:318.1-318.25
   def $exportsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:314.1-314.56
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:319.1-319.56
   def $exportsd{export : export, `decl'*` : decl*}([(export : export <: decl)] ++ decl'*{decl' <- `decl'*`}) = [export] ++ $exportsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:315.1-315.61
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:320.1-320.61
   def $exportsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $exportsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -20050,16 +20053,19 @@ grammar Btypesec : type*
   prod{`ty*` : type*} ty*{ty <- `ty*`}:Bsection_(1, syntax type, grammar Blist(syntax type, grammar Btype)) => ty*{ty <- `ty*`}
 
 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
-grammar Bimport : (name, externtype)
+grammar Bimportitem : (name, externtype)
   ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
   prod{nm_2 : name, xt : externtype} {{nm_2:Bname} {xt:Bexterntype}} => (nm_2, xt)
 
 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
 grammar Bimports : import*
   ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
-  prod{nm_1 : name, nm_2 : name, xt : externtype} {{nm_1:Bname} {(nm_2, xt):Bimport}} => [IMPORT_import(nm_1, nm_2, xt)]
+  prod{nm_1 : name, nm_2 : name, xt : externtype} {{nm_1:Bname} {nm_2:Bname} {xt:Bexterntype}} => [IMPORT_import(nm_1, nm_2, xt)]
+  ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
+  prod{nm_1 : name, nm_e : name, `nm_2*` : name*, `xt*` : externtype*} {{nm_1:Bname} {nm_e:Bname} {0x7F} {(nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}:Blist(syntax (name, externtype), grammar Bimportitem)}} => IMPORT_import(nm_1, nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}
+    -- if (nm_e = `%`_name([]))
   ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
-  prod{nm_1 : name, nm_e : name, `nm_2*` : name*, `xt*` : externtype*} {{nm_1:Bname} {nm_e:Bname} {0x7F} {(nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}:Blist(syntax (name, externtype), grammar Bimport)}} => IMPORT_import(nm_1, nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}
+  prod{nm_1 : name, nm_e : name, xt : externtype, `nm_2*` : name*} {{nm_1:Bname} {nm_e:Bname} {0x7E} {xt:Bexterntype} {nm_2*{nm_2 <- `nm_2*`}:Blist(syntax name, grammar Bname)}} => IMPORT_import(nm_1, nm_2, xt)*{nm_2 <- `nm_2*`}
     -- if (nm_e = `%`_name([]))
 
 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
@@ -22316,13 +22322,13 @@ syntax decl =
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:261.1-261.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:266.1-266.76
 def $typesd(decl*) : type*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:273.1-273.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:278.1-278.23
   def $typesd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:274.1-274.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:279.1-279.48
   def $typesd{type : type, `decl'*` : decl*}([(type : type <: decl)] ++ decl'*{decl' <- `decl'*`}) = [type] ++ $typesd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:275.1-275.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:280.1-280.57
   def $typesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $typesd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -22330,13 +22336,13 @@ def $typesd(decl*) : type*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:262.1-262.78
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:267.1-267.78
 def $importsd(decl*) : import*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:277.1-277.25
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:282.1-282.25
   def $importsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:278.1-278.56
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:283.1-283.56
   def $importsd{import : import, `decl'*` : decl*}([(import : import <: decl)] ++ decl'*{decl' <- `decl'*`}) = [import] ++ $importsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:279.1-279.61
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:284.1-284.61
   def $importsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $importsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -22344,13 +22350,13 @@ def $importsd(decl*) : import*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:263.1-263.75
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:268.1-268.75
 def $tagsd(decl*) : tag*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:281.1-281.22
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:286.1-286.22
   def $tagsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:282.1-282.44
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:287.1-287.44
   def $tagsd{tag : tag, `decl'*` : decl*}([(tag : tag <: decl)] ++ decl'*{decl' <- `decl'*`}) = [tag] ++ $tagsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:283.1-283.55
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:288.1-288.55
   def $tagsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tagsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -22358,13 +22364,13 @@ def $tagsd(decl*) : tag*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:264.1-264.78
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:269.1-269.78
 def $globalsd(decl*) : global*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:285.1-285.25
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:290.1-290.25
   def $globalsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:286.1-286.56
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:291.1-291.56
   def $globalsd{global : global, `decl'*` : decl*}([(global : global <: decl)] ++ decl'*{decl' <- `decl'*`}) = [global] ++ $globalsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:287.1-287.61
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:292.1-292.61
   def $globalsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $globalsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -22372,13 +22378,13 @@ def $globalsd(decl*) : global*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:265.1-265.75
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:270.1-270.75
 def $memsd(decl*) : mem*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:289.1-289.22
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:294.1-294.22
   def $memsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:290.1-290.44
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:295.1-295.44
   def $memsd{mem : mem, `decl'*` : decl*}([(mem : mem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [mem] ++ $memsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:291.1-291.55
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:296.1-296.55
   def $memsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $memsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -22386,13 +22392,13 @@ def $memsd(decl*) : mem*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:266.1-266.77
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:271.1-271.77
 def $tablesd(decl*) : table*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:293.1-293.24
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:298.1-298.24
   def $tablesd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:294.1-294.52
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:299.1-299.52
   def $tablesd{table : table, `decl'*` : decl*}([(table : table <: decl)] ++ decl'*{decl' <- `decl'*`}) = [table] ++ $tablesd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:295.1-295.59
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:300.1-300.59
   def $tablesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tablesd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -22400,13 +22406,13 @@ def $tablesd(decl*) : table*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:267.1-267.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:272.1-272.76
 def $funcsd(decl*) : func*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:297.1-297.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:302.1-302.23
   def $funcsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:298.1-298.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:303.1-303.48
   def $funcsd{func : func, `decl'*` : decl*}([(func : func <: decl)] ++ decl'*{decl' <- `decl'*`}) = [func] ++ $funcsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:299.1-299.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:304.1-304.57
   def $funcsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $funcsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -22414,13 +22420,13 @@ def $funcsd(decl*) : func*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:268.1-268.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:273.1-273.76
 def $datasd(decl*) : data*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:301.1-301.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:306.1-306.23
   def $datasd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:302.1-302.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:307.1-307.48
   def $datasd{data : data, `decl'*` : decl*}([(data : data <: decl)] ++ decl'*{decl' <- `decl'*`}) = [data] ++ $datasd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:303.1-303.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:308.1-308.57
   def $datasd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $datasd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -22428,13 +22434,13 @@ def $datasd(decl*) : data*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:269.1-269.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:274.1-274.76
 def $elemsd(decl*) : elem*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:305.1-305.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:310.1-310.23
   def $elemsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:306.1-306.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:311.1-311.48
   def $elemsd{elem : elem, `decl'*` : decl*}([(elem : elem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [elem] ++ $elemsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:307.1-307.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:312.1-312.57
   def $elemsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $elemsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -22442,13 +22448,13 @@ def $elemsd(decl*) : elem*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:270.1-270.77
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:275.1-275.77
 def $startsd(decl*) : start*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:309.1-309.24
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:314.1-314.24
   def $startsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:310.1-310.52
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:315.1-315.52
   def $startsd{start : start, `decl'*` : decl*}([(start : start <: decl)] ++ decl'*{decl' <- `decl'*`}) = [start] ++ $startsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:311.1-311.59
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:316.1-316.59
   def $startsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $startsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -22456,13 +22462,13 @@ def $startsd(decl*) : start*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:271.1-271.78
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:276.1-276.78
 def $exportsd(decl*) : export*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:313.1-313.25
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:318.1-318.25
   def $exportsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:314.1-314.56
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:319.1-319.56
   def $exportsd{export : export, `decl'*` : decl*}([(export : export <: decl)] ++ decl'*{decl' <- `decl'*`}) = [export] ++ $exportsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:315.1-315.61
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:320.1-320.61
   def $exportsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $exportsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -31581,16 +31587,19 @@ grammar Btypesec : type*
   prod{`ty*` : type*} ty*{ty <- `ty*`}:Bsection_(1, syntax type, grammar Blist(syntax type, grammar Btype)) => ty*{ty <- `ty*`}
 
 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
-grammar Bimport : (name, externtype)
+grammar Bimportitem : (name, externtype)
   ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
   prod{nm_2 : name, xt : externtype} {{nm_2:Bname} {xt:Bexterntype}} => (nm_2, xt)
 
 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
 grammar Bimports : import*
   ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
-  prod{nm_1 : name, nm_2 : name, xt : externtype} {{nm_1:Bname} {(nm_2, xt):Bimport}} => [IMPORT_import(nm_1, nm_2, xt)]
+  prod{nm_1 : name, nm_2 : name, xt : externtype} {{nm_1:Bname} {nm_2:Bname} {xt:Bexterntype}} => [IMPORT_import(nm_1, nm_2, xt)]
+  ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
+  prod{nm_1 : name, nm_e : name, `nm_2*` : name*, `xt*` : externtype*} {{nm_1:Bname} {nm_e:Bname} {0x7F} {(nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}:Blist(syntax (name, externtype), grammar Bimportitem)}} => IMPORT_import(nm_1, nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}
+    -- if (nm_e = `%`_name([]))
   ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
-  prod{nm_1 : name, nm_e : name, `nm_2*` : name*, `xt*` : externtype*} {{nm_1:Bname} {nm_e:Bname} {0x7F} {(nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}:Blist(syntax (name, externtype), grammar Bimport)}} => IMPORT_import(nm_1, nm_2, xt)*{nm_2 <- `nm_2*`, xt <- `xt*`}
+  prod{nm_1 : name, nm_e : name, xt : externtype, `nm_2*` : name*} {{nm_1:Bname} {nm_e:Bname} {0x7E} {xt:Bexterntype} {nm_2*{nm_2 <- `nm_2*`}:Blist(syntax name, grammar Bname)}} => IMPORT_import(nm_1, nm_2, xt)*{nm_2 <- `nm_2*`}
     -- if (nm_e = `%`_name([]))
 
 ;; ../../../../specification/wasm-3.0/5.4-binary.modules.spectec
@@ -33847,13 +33856,13 @@ syntax decl =
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:261.1-261.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:266.1-266.76
 def $typesd(decl*) : type*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:273.1-273.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:278.1-278.23
   def $typesd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:274.1-274.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:279.1-279.48
   def $typesd{type : type, `decl'*` : decl*}([(type : type <: decl)] ++ decl'*{decl' <- `decl'*`}) = [type] ++ $typesd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:275.1-275.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:280.1-280.57
   def $typesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $typesd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -33861,13 +33870,13 @@ def $typesd(decl*) : type*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:262.1-262.78
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:267.1-267.78
 def $importsd(decl*) : import*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:277.1-277.25
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:282.1-282.25
   def $importsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:278.1-278.56
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:283.1-283.56
   def $importsd{import : import, `decl'*` : decl*}([(import : import <: decl)] ++ decl'*{decl' <- `decl'*`}) = [import] ++ $importsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:279.1-279.61
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:284.1-284.61
   def $importsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $importsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -33875,13 +33884,13 @@ def $importsd(decl*) : import*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:263.1-263.75
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:268.1-268.75
 def $tagsd(decl*) : tag*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:281.1-281.22
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:286.1-286.22
   def $tagsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:282.1-282.44
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:287.1-287.44
   def $tagsd{tag : tag, `decl'*` : decl*}([(tag : tag <: decl)] ++ decl'*{decl' <- `decl'*`}) = [tag] ++ $tagsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:283.1-283.55
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:288.1-288.55
   def $tagsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tagsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -33889,13 +33898,13 @@ def $tagsd(decl*) : tag*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:264.1-264.78
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:269.1-269.78
 def $globalsd(decl*) : global*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:285.1-285.25
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:290.1-290.25
   def $globalsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:286.1-286.56
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:291.1-291.56
   def $globalsd{global : global, `decl'*` : decl*}([(global : global <: decl)] ++ decl'*{decl' <- `decl'*`}) = [global] ++ $globalsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:287.1-287.61
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:292.1-292.61
   def $globalsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $globalsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -33903,13 +33912,13 @@ def $globalsd(decl*) : global*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:265.1-265.75
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:270.1-270.75
 def $memsd(decl*) : mem*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:289.1-289.22
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:294.1-294.22
   def $memsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:290.1-290.44
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:295.1-295.44
   def $memsd{mem : mem, `decl'*` : decl*}([(mem : mem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [mem] ++ $memsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:291.1-291.55
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:296.1-296.55
   def $memsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $memsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -33917,13 +33926,13 @@ def $memsd(decl*) : mem*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:266.1-266.77
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:271.1-271.77
 def $tablesd(decl*) : table*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:293.1-293.24
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:298.1-298.24
   def $tablesd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:294.1-294.52
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:299.1-299.52
   def $tablesd{table : table, `decl'*` : decl*}([(table : table <: decl)] ++ decl'*{decl' <- `decl'*`}) = [table] ++ $tablesd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:295.1-295.59
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:300.1-300.59
   def $tablesd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $tablesd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -33931,13 +33940,13 @@ def $tablesd(decl*) : table*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:267.1-267.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:272.1-272.76
 def $funcsd(decl*) : func*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:297.1-297.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:302.1-302.23
   def $funcsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:298.1-298.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:303.1-303.48
   def $funcsd{func : func, `decl'*` : decl*}([(func : func <: decl)] ++ decl'*{decl' <- `decl'*`}) = [func] ++ $funcsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:299.1-299.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:304.1-304.57
   def $funcsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $funcsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -33945,13 +33954,13 @@ def $funcsd(decl*) : func*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:268.1-268.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:273.1-273.76
 def $datasd(decl*) : data*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:301.1-301.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:306.1-306.23
   def $datasd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:302.1-302.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:307.1-307.48
   def $datasd{data : data, `decl'*` : decl*}([(data : data <: decl)] ++ decl'*{decl' <- `decl'*`}) = [data] ++ $datasd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:303.1-303.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:308.1-308.57
   def $datasd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $datasd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -33959,13 +33968,13 @@ def $datasd(decl*) : data*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:269.1-269.76
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:274.1-274.76
 def $elemsd(decl*) : elem*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:305.1-305.23
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:310.1-310.23
   def $elemsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:306.1-306.48
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:311.1-311.48
   def $elemsd{elem : elem, `decl'*` : decl*}([(elem : elem <: decl)] ++ decl'*{decl' <- `decl'*`}) = [elem] ++ $elemsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:307.1-307.57
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:312.1-312.57
   def $elemsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $elemsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -33973,13 +33982,13 @@ def $elemsd(decl*) : elem*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:270.1-270.77
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:275.1-275.77
 def $startsd(decl*) : start*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:309.1-309.24
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:314.1-314.24
   def $startsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:310.1-310.52
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:315.1-315.52
   def $startsd{start : start, `decl'*` : decl*}([(start : start <: decl)] ++ decl'*{decl' <- `decl'*`}) = [start] ++ $startsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:311.1-311.59
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:316.1-316.59
   def $startsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $startsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
@@ -33987,13 +33996,13 @@ def $startsd(decl*) : start*
 ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec
 rec {
 
-;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:271.1-271.78
+;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:276.1-276.78
 def $exportsd(decl*) : export*
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:313.1-313.25
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:318.1-318.25
   def $exportsd([]) = []
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:314.1-314.56
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:319.1-319.56
   def $exportsd{export : export, `decl'*` : decl*}([(export : export <: decl)] ++ decl'*{decl' <- `decl'*`}) = [export] ++ $exportsd(decl'*{decl' <- `decl'*`})
-  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:315.1-315.61
+  ;; ../../../../specification/wasm-3.0/6.3-text.modules.spectec:320.1-320.61
   def $exportsd{decl : decl, `decl'*` : decl*}([decl] ++ decl'*{decl' <- `decl'*`}) = $exportsd(decl'*{decl' <- `decl'*`})
     -- otherwise
 }
diff --git a/spectec/test-splice/TEST.md b/spectec/test-splice/TEST.md
index db9142492..ac79aa143 100644
--- a/spectec/test-splice/TEST.md
+++ b/spectec/test-splice/TEST.md
@@ -545,7 +545,7 @@ warning: grammar `Bglobalsec` was never spliced
 warning: grammar `Bglobaltype` was never spliced
 warning: grammar `Bheaptype` was never spliced
 warning: grammar `BiN` was never spliced
-warning: grammar `Bimport` was never spliced
+warning: grammar `Bimportitem` was never spliced
 warning: grammar `Bimports` was never spliced
 warning: grammar `Bimportsec` was never spliced
 warning: grammar `Binstr/parametric` was never spliced
@@ -769,7 +769,8 @@ warning: grammar `Timport_/abbrev-mem` was never spliced
 warning: grammar `Timport_/abbrev-table` was never spliced
 warning: grammar `Timport_/abbrev-func` was never spliced
 warning: grammar `Timportdots` was never spliced
-warning: grammar `Timports_/abbrev` was never spliced
+warning: grammar `Timports_/abbrev-compact1` was never spliced
+warning: grammar `Timports_/abbrev-compact2` was never spliced
 warning: grammar `Tinstr_` was never spliced
 warning: grammar `Tinstrs_/unfolded` was never spliced
 warning: grammar `Tinstrs_/folded` was never spliced