From c1a61a192cff022800681b0c14d6c0413ba0cf2a Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 27 Oct 2005 08:49:12 +0000
Subject: [PATCH] typing errors

---
 helm/ocaml/tactics/doc/main.tex | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/helm/ocaml/tactics/doc/main.tex b/helm/ocaml/tactics/doc/main.tex
index 19c136f2a..d812bcd33 100644
--- a/helm/ocaml/tactics/doc/main.tex
+++ b/helm/ocaml/tactics/doc/main.tex
@@ -52,7 +52,7 @@
 \newcommand{\ISOPEN}{\MATHIT{is\_open}}
 \newcommand{\DEEPCLOSE}{\MATHIT{deep\_close}}
 \newcommand{\REMOVEGOALS}{\MATHIT{remove\_goals}}
-\newcommand{\GOALS}{\MATHIT{goals}}
+\newcommand{\GOALS}{\MATHIT{open\_goals}}
 
 \newcommand{\BRANCHTAG}{\ensuremath{\mathtt{B}}}
 \newcommand{\FOCUSTAG}{\ensuremath{\mathtt{F}}}
@@ -115,7 +115,7 @@
  \item $\ZEROPOS([g_1;\cdots;g_n]) =
   [\langle 0,\OPEN~g_1\rangle;\cdots;\langle 0,\OPEN~g_n\rangle]$
  \item $\INITPOS([\langle i_1,s_1\rangle;\cdots;\langle i_n,s_n\rangle]) =
-  [\langle 1,\OPEN~s_1\rangle;\cdots;\langle n,\OPEN~s_n\rangle]$
+  [\langle 1,s_1\rangle;\cdots;\langle n,s_n\rangle]$
  \item $\ISFRESH(s) =
   \left\{
   \begin{array}{ll}
@@ -149,7 +149,7 @@
   that each locator whose goal is in $G$ is marked as closed in $\Gamma$ stack
   components and removed from $\tau$ and $\kappa$ components.
  \item $\GOALS(S)$: (inutition) return all goals appearing in whatever position
-  on a given stack $S$.
+  on a given stack $S$, appearing in an \OPEN{} switch.
 \end{itemize}
 
 \paragraph{Invariants}
@@ -158,6 +158,8 @@
   \in\tau\cup\kappa, \exists g, s = \OPEN~g$ (each locator on the stack in
   $\tau$ and $\kappa$ components has an \OPEN~switch).
  \item Unless \FOCUS{} is used the stack contains no duplicate goals.
+ \item $\forall~\mathrm{locator}~l\in\Gamma \mbox{(with the exception of the
+  top-level $\Gamma$)}, \ISFRESH(l)$.
 \end{itemize}
 
 \subsection{Semantics}
@@ -292,7 +294,7 @@
 
  \SEM{\FOCUS{g_1,\dots,g_n}}{S}
  & = 
- & \langle \xi, \ENTRY{[\OPEN~g_1;\cdots;\OPEN~g_n]}{[]}{[]}{\FOCUSTAG}
+ & \langle \xi, \ENTRY{\ZEROPOS([g_1;\cdots;g_n])}{[]}{[]}{\FOCUSTAG}
    ::\DEEPCLOSE(S)
    \rangle
  \\[1ex]
-- 
2.39.2