chore: adapt to where syntax change

leanprover · Jun 17, 2022 · 8eb2236 · 8eb2236
1 parent 521d064
commit 8eb2236
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 6 deletions.
diff --git a/Lake/DSL/Package.lean b/Lake/DSL/Package.lean
@@ -42,15 +42,15 @@ def mkPackageDecl (doc? : Option Syntax) (attrs : Array Syntax) : Macro
 | `(packageDeclSpec| $id:ident) =>
   `($[$doc?:docComment]? @[$attrs,*] def $(mkIdentFrom id packageDeclName) : PackageConfig :=
     {name := $(quote id.getId)})
-| `(packageDeclSpec| $id:ident where $[$ds]* $[$wds?]?) =>
+| `(packageDeclSpec| $id:ident where $ds;* $[$wds?]?) =>
   `($[$doc?:docComment]? @[$attrs,*] def $(mkIdentFrom id packageDeclName) : PackageConfig where
-      name := $(quote id.getId) $[$ds]* $[$wds?]?)
+      name := $(quote id.getId); $ds;* $[$wds?]?)
 | `(packageDeclSpec| $id:ident : $ty := $defn $[$wds?]?) =>
   `($[$doc?:docComment]? @[$attrs,*] def $(mkIdentFrom id packageDeclName) : $ty := $defn $[$wds?]?)
 | `(packageDeclSpec| $id:ident $[($dir?)]? $[($args?)]? := $defn $[$wds?]?) =>
   mkSimplePackageDecl doc? attrs (mkIdentFrom id packageDeclName) defn dir? args? wds?
 | `(packageDeclSpec| $id:ident $[($dir?)]? $[($args?)]? { $[$fs $[,]?]* } $[$wds?]?) => do
-  let defn ← `({ name := $(quote id.getId), $[$fs]* })
+  let defn ← `({ name := $(quote id.getId), $fs,* })
   mkSimplePackageDecl doc? attrs (mkIdentFrom id packageDeclName) defn dir? args? wds?
 | `(packageDeclSpec| $id:ident $[($dir?)]? $[($args?)]? do $seq $[$wds?]?) => do
   let (_, dir, args) ← expandPackageBinders dir? args?

diff --git a/Lake/DSL/Targets.lean b/Lake/DSL/Targets.lean
@@ -23,13 +23,13 @@ def mkTargetDecl
 | `(targetDeclSpec| $id:ident) =>
   `($[$doc?:docComment]? @[$attrs,*] def $id : $ty :=
     {name := $(quote id.getId)})
-| `(targetDeclSpec| $id:ident where $[$ds]* $[$wds?]?) =>
+| `(targetDeclSpec| $id:ident where $ds;* $[$wds?]?) =>
   `($[$doc?:docComment]? @[$attrs,*] def $id : $ty where
-      name := $(quote id.getId) $[$ds]* $[$wds?]?)
+      name := $(quote id.getId); $ds;* $[$wds?]?)
 | `(targetDeclSpec| $id:ident $[: $ty?]? := $defn $[$wds?]?) =>
   `($[$doc?:docComment]? @[$attrs,*] def $id : $(ty?.getD ty) := $defn $[$wds?]?)
 | `(targetDeclSpec| $id:ident { $[$fs $[,]?]* } $[$wds?]?) => do
-  let defn ← `({ name := $(quote id.getId), $[$fs]* })
+  let defn ← `({ name := $(quote id.getId), $fs,* })
   `($[$doc?:docComment]? @[$attrs,*] def $id : $ty := $defn $[$wds?]?)
 | stx => Macro.throwErrorAt stx "ill-formed target declaration"