From f8a1cdc888af88989641385ef78d213c66bdc260 Mon Sep 17 00:00:00 2001
From: Hans-Joerg Schurr <commits@schurr.at>
Date: Wed, 8 May 2024 11:03:38 -0500
Subject: [PATCH] Fix context description in subproof closing rules.

Addresses https://gitlab.uliege.be/verit/alethe/-/issues/36
---
 spec/changelog.tex | 2 ++
 spec/rule_list.tex | 8 ++++----
 2 files changed, 6 insertions(+), 4 deletions(-)

diff --git a/spec/changelog.tex b/spec/changelog.tex
index 0da3149..5b76a0a 100644
--- a/spec/changelog.tex
+++ b/spec/changelog.tex
@@ -24,6 +24,8 @@ Clarifications and corrected errors:
   \item Fix mistake in proof grammar.  It now uses the \texttt{context\_annotation}
         non-terminal in the rule for the \texttt{anchor} command.
   \item Fix the example of \proofRule{onepoint}.
+  \item Add the missing context to the conclusion of \proofRule{bind},
+        \proofRule{sko_ex}, \proofRule{sko_forall}, \proofRule{onepoint}.
 \end{itemize}
 
 \subsection*{0.3 --- \DTMdisplaydate{2023}{02}{10}{-1}}
diff --git a/spec/rule_list.tex b/spec/rule_list.tex
index 1266d48..528e776 100644
--- a/spec/rule_list.tex
+++ b/spec/rule_list.tex
@@ -550,7 +550,7 @@ as for the rule \proofRule{la_generic}.
 $j$. & \spctx{ $\Gamma, y_1,\dots, y_n,  x_1 \mapsto y_1, \dots ,  x_n \mapsto y_n$}
    & \ctxsep & $\varphi ≈ \varphi'$ & ($\dots$) \\
    \spsep
-$k$. & & \ctxsep &
+$k$. & $\Gamma$ & \ctxsep &
     $\forall x_1, \dots, x_n.\varphi ≈ \forall y_1, \dots, y_n. \varphi'$
      & \currule{} \\
 \end{AletheXS}
@@ -567,7 +567,7 @@ $j$. &
 \spctx{$\Gamma, x_1 \mapsto \varepsilon_1, \dots ,  x_n \mapsto \varepsilon_n$}
    & \ctxsep &  $\varphi ≈ \psi$ & ($\dots$) \\
    \spsep
-$k$. & & \ctxsep & $\exists x_1, \dots, x_n.\varphi ≈ \psi$ & \currule{} \\
+$k$. & $\Gamma$ & \ctxsep & $\exists x_1, \dots, x_n.\varphi ≈ \psi$ & \currule{} \\
 \end{AletheXS}
 where $\varepsilon_i$ stands for $\varepsilon x_i. (\exists x_{i+1}, \dots,
 x_n. \varphi)$.
@@ -582,7 +582,7 @@ $j$. &
 \spctx{$\Gamma, x_1 \mapsto (\varepsilon x_1.\neg\varphi), \dots,  x_n \mapsto (\varepsilon x_n.\neg\varphi)$}
    & \ctxsep & $\varphi ≈ \psi$ & ($\dots$) \\
  \spsep
-$k$. & & \ctxsep  & $\forall x_1, \dots, x_n.\varphi ≈ \psi$ & \currule{} \\
+$k$. & $\Gamma$ & \ctxsep  & $\forall x_1, \dots, x_n.\varphi ≈ \psi$ & \currule{} \\
 \end{AletheXS}
 
 \end{RuleDescription}
@@ -1206,7 +1206,7 @@ variables that can only have one value.
 $j$. & \spctx{$\Gamma, x_{k_1},\dots, x_{k_m},  x_{j_1} \mapsto t_{j_1}, \dots ,  x_{j_o} \mapsto t_{j_o}$}
    & \ctxsep & $\varphi ≈ \varphi'$ & ($\dots$) \\
  \spsep
-$k$. & & \ctxsep  & $Q x_1, \dots, x_n.\varphi ≈ Q x_{k_1}, \dots, x_{k_m}. \varphi'$ & \currule{} \\
+$k$. & $\Gamma$ & \ctxsep  & $Q x_1, \dots, x_n.\varphi ≈ Q x_{k_1}, \dots, x_{k_m}. \varphi'$ & \currule{} \\
 \end{AletheXS}
 where $Q\in\{\forall, \exists\}$,  $n = m + o$,  $k_1, \dots, k_m$ and
 $j_1, \dots, j_o$ are monotone
-- 
GitLab