From c78ecd0c99a5bcab9041704d1abbb28d81a601ab Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Thu, 23 May 2024 19:16:33 +0200
Subject: [PATCH] CI

---
 spectec/test-frontend/TEST.md |  5 -----
 spectec/test-latex/TEST.md    |  8 --------
 spectec/test-middlend/TEST.md | 25 -------------------------
 spectec/test-prose/TEST.md    |  3 ---
 spectec/test-splice/TEST.md   |  2 --
 5 files changed, 43 deletions(-)

diff --git a/spectec/test-frontend/TEST.md b/spectec/test-frontend/TEST.md
index 6d13c5e997..269aa0e690 100644
--- a/spectec/test-frontend/TEST.md
+++ b/spectec/test-frontend/TEST.md
@@ -67,11 +67,6 @@ def $concat_(syntax X, X**) : X*
   def $concat_{syntax X, w* : X*, w'** : X**}(syntax X, [w*{w : X}] :: w'*{w' : X}*{w' : X}) = w*{w : X} :: $concat_(syntax X, w'*{w' : X}*{w' : X})
 }
 
-;; 0-aux.watsup
-def $skip(syntax X, X : X) : X
-  ;; 0-aux.watsup
-  def $skip{syntax X, w : X}(syntax X, w) = w
-
 ;; 1-syntax.watsup
 syntax list{syntax X}(syntax X) =
   | `%`{X* : X*}(X*{X : X} : X*)
diff --git a/spectec/test-latex/TEST.md b/spectec/test-latex/TEST.md
index e980d27e95..72df6d22e5 100644
--- a/spectec/test-latex/TEST.md
+++ b/spectec/test-latex/TEST.md
@@ -1308,14 +1308,6 @@ $$
 \end{array}
 $$
 
-\vspace{1ex}
-
-$$
-\begin{array}{@{}lcl@{}l@{}}
- &=& w \\
-\end{array}
-$$
-
 $$
 \begin{array}{@{}lrrl@{}l@{}}
 & {\mathit{list}}({\mathit{{\scriptstyle X}}}) &::=& {{\mathit{{\scriptstyle X}}}^\ast}
diff --git a/spectec/test-middlend/TEST.md b/spectec/test-middlend/TEST.md
index 8483e9671c..5c73d323ab 100644
--- a/spectec/test-middlend/TEST.md
+++ b/spectec/test-middlend/TEST.md
@@ -57,11 +57,6 @@ def $concat_(syntax X, X**) : X*
   def $concat_{syntax X, w* : X*, w'** : X**}(syntax X, [w*{w : X}] :: w'*{w' : X}*{w' : X}) = w*{w : X} :: $concat_(syntax X, w'*{w' : X}*{w' : X})
 }
 
-;; 0-aux.watsup
-def $skip(syntax X, X : X) : X
-  ;; 0-aux.watsup
-  def $skip{syntax X, w : X}(syntax X, w) = w
-
 ;; 1-syntax.watsup
 syntax list{syntax X}(syntax X) =
   | `%`{X* : X*}(X*{X : X} : X*)
@@ -5753,11 +5748,6 @@ def $concat_(syntax X, X**) : X*
   def $concat_{syntax X, w* : X*, w'** : X**}(syntax X, [w*{w : X}] :: w'*{w' : X}*{w' : X}) = w*{w : X} :: $concat_(syntax X, w'*{w' : X}*{w' : X})
 }
 
-;; 0-aux.watsup
-def $skip(syntax X, X : X) : X
-  ;; 0-aux.watsup
-  def $skip{syntax X, w : X}(syntax X, w) = w
-
 ;; 1-syntax.watsup
 syntax list{syntax X}(syntax X) =
   | `%`{X* : X*}(X*{X : X} : X*)
@@ -11454,11 +11444,6 @@ def $concat_(syntax X, X**) : X*
   def $concat_{syntax X, w* : X*, w'** : X**}(syntax X, [w*{w : X}] :: w'*{w' : X}*{w' : X}) = w*{w : X} :: $concat_(syntax X, w'*{w' : X}*{w' : X})
 }
 
-;; 0-aux.watsup
-def $skip(syntax X, X : X) : X
-  ;; 0-aux.watsup
-  def $skip{syntax X, w : X}(syntax X, w) = w
-
 ;; 1-syntax.watsup
 syntax list{syntax X}(syntax X) =
   | `%`{X* : X*}(X*{X : X} : X*)
@@ -17155,11 +17140,6 @@ def $concat_(syntax X, X**) : X*
   def $concat_{syntax X, w* : X*, w'** : X**}(syntax X, [w*{w : X}] :: w'*{w' : X}*{w' : X}) = w*{w : X} :: $concat_(syntax X, w'*{w' : X}*{w' : X})
 }
 
-;; 0-aux.watsup
-def $skip(syntax X, X : X) : X
-  ;; 0-aux.watsup
-  def $skip{syntax X, w : X}(syntax X, w) = w
-
 ;; 1-syntax.watsup
 syntax list{syntax X}(syntax X) =
   | `%`{X* : X*}(X*{X : X} : X*)
@@ -23009,11 +22989,6 @@ def $concat_(syntax X, X**) : X*
   def $concat_{syntax X, w* : X*, w'** : X**}(syntax X, [w*{w : X}] :: w'*{w' : X}*{w' : X}) = w*{w : X} :: $concat_(syntax X, w'*{w' : X}*{w' : X})
 }
 
-;; 0-aux.watsup
-def $skip(syntax X, X : X) : X
-  ;; 0-aux.watsup
-  def $skip{syntax X, w : X}(syntax X, w) = w
-
 ;; 1-syntax.watsup
 syntax list{syntax X}(syntax X) =
   | `%`{X* : X*}(X*{X : X} : X*)
diff --git a/spectec/test-prose/TEST.md b/spectec/test-prose/TEST.md
index 1fbc784225..c596417cbd 100644
--- a/spectec/test-prose/TEST.md
+++ b/spectec/test-prose/TEST.md
@@ -4161,9 +4161,6 @@ concat_ X_u0*
 2. Let [w*] ++ w'** be X_u0*.
 3. Return w* ++ $concat_(w'**).
 
-skip w
-1. Return w.
-
 signif N_u0
 1. If (N_u0 is 32), then:
   a. Return 23.
diff --git a/spectec/test-splice/TEST.md b/spectec/test-splice/TEST.md
index 2e42f5cfa8..ccc8de7cdf 100644
--- a/spectec/test-splice/TEST.md
+++ b/spectec/test-splice/TEST.md
@@ -1239,7 +1239,6 @@ warning: definition `signif` was never spliced
 warning: definition `sizenn` was never spliced
 warning: definition `sizenn1` was never spliced
 warning: definition `sizenn2` was never spliced
-warning: definition `skip` was never spliced
 warning: definition `store` was never spliced
 warning: definition `structinst` was never spliced
 warning: definition `subst_all_deftype` was never spliced
@@ -1631,7 +1630,6 @@ warning: definition prose `size` was never spliced
 warning: definition prose `sizenn` was never spliced
 warning: definition prose `sizenn1` was never spliced
 warning: definition prose `sizenn2` was never spliced
-warning: definition prose `skip` was never spliced
 warning: definition prose `store` was never spliced
 warning: definition prose `structinst` was never spliced
 warning: definition prose `subst_all_deftype` was never spliced