From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 27 Oct 2005 08:49:12 +0000 (+0000)
Subject: typing errors
X-Git-Tag: V_0_7_2_3~179
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c1a61a192cff022800681b0c14d6c0413ba0cf2a;p=helm.git

typing errors
---

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]