typing errors

diff --git a/helm/ocaml/tactics/doc/main.tex b/helm/ocaml/tactics/doc/main.tex
index 19c136f2a6aac3f82b62caf4cd06c77c3367bec5..d812bcd334ee484fe6569903c1e0c3351bb27d23 100644 (file)
--- 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]