From: Stefano Zacchiroli 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]