From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 30 Sep 2005 14:16:28 +0000 (+0000)
Subject: fixed some (more) typos
X-Git-Tag: V_0_7_2_3~271
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=36748e60ec1575b946a9eefd8f6490f9bac2667b;p=helm.git

fixed some (more) typos
---

diff --git a/helm/ocaml/tactics/doc/main.tex b/helm/ocaml/tactics/doc/main.tex
index b2996c116..1cc0dadd9 100644
--- a/helm/ocaml/tactics/doc/main.tex
+++ b/helm/ocaml/tactics/doc/main.tex
@@ -116,18 +116,18 @@
  & \langle\xi_n,\MAPOPEN{G^O_n}::\DEEPCLOSE{G^C_n,\Gamma},\tau,\kappa\rangle
  \\[1ex]
 
- \multicolumn{3}{l}{\hspace{2em}
+ \multicolumn{3}{l}{\hspace{2em}\mathit{where} ~
  \left\{
  \begin{array}{rcll}
   \langle\xi_0, G^O_0, G^C_0\rangle & = & \langle\xi, [], []\rangle \\
   \langle\xi_{i+1}, G^O_{i+1}, G^C_{i+1}\rangle
   & =
   & \langle\xi_i, G^O_i, G^C_i\rangle
-  & g_i\in G^C_i \\
+  & g_{i+1}\in G^C_i \\
   \langle\xi_{i+1}, G^O_{i+1}, G^C_{i+1}\rangle
   & =
   & \langle\xi, (G^O_i\setminus G^C)\cup G^O, G^C_i\cup G^C\rangle
-  & g_i\not\in G^C_i \\
+  & g_{i+1}\not\in G^C_i \\
   & & \mathit{where} ~ \langle\xi,G^O,G^C\rangle=\TSEM{T}{\xi_i}{g_{i+1}}
   \\
  \end{array}