fixed some typos

diff --git a/helm/ocaml/tactics/doc/main.tex b/helm/ocaml/tactics/doc/main.tex
index 43e17ebe8599de8b914e67f8dfc76a9b4de0a06c..b2996c11609edd25e076723cadd197b181ff3a1e 100644 (file)
--- a/helm/ocaml/tactics/doc/main.tex
+++ b/helm/ocaml/tactics/doc/main.tex
@@ -71,7 +71,7 @@
  \mathit{status} & = & \xi\times\Gamma\times\tau\times\kappa & \\
  \xi & & & \mbox{(metasenv)} \\
  \Gamma & = & \GOALSWITCH~\LIST~\STACK & \mbox{(context)} \\
- \GOALSWITCH & = & \OPEN{g} \quad | \quad \CLOSED{g} & \\
+ \GOALSWITCH & = & \OPEN{n} \quad | \quad \CLOSED{n} & \\
  \tau & = & \GOAL~\LIST~\STACK & \mbox{(todo)} \\
  \kappa & = & \GOAL~\LIST~\STACK & \mbox{(dot continuations)} \\
 \end{array}
@@ -103,9 +103,9 @@
 
 \[
 \begin{array}{rlcc}
- \TSEM{\APPLY{tac}}{\xi}{\OPEN{g}} & =
- & \mathit{apply\_tac}(\mathit{tac},\xi,g) & \\
- \TSEM{\SKIP}{\xi}{\CLOSED{g}} & = & \langle [], [g]\rangle & \\
+ \TSEM{\APPLY{tac}}{\xi}{\OPEN{n}} & =
+ & \mathit{apply\_tac}(\mathit{tac},\xi,n) & \\
+ \TSEM{\SKIP}{\xi}{\CLOSED{n}} & = & \langle [], [n]\rangle & \\
 \end{array}
 \]
 
@@ -151,9 +151,9 @@
    (\FILTEROPEN{G}\cup K)::\kappa\rangle
  \\[2ex]
 
- \SEM{~\DOT~}{\xi}{[]::\Gamma}{\tau}{(g::G)::\kappa}
+ \SEM{~\DOT~}{\xi}{[]::\Gamma}{\tau}{(n::N)::\kappa}
  & =
- & \langle\xi, [g]::\Gamma, \tau, G::\kappa\rangle
+ & \langle\xi, [\OPEN{n}]::\Gamma, \tau, N::\kappa\rangle
  \\[2ex]
 
  \SEM{~\BRANCH~}{\xi}{[g_1;\dots;g_n]::\Gamma}{\tau}{\kappa}
@@ -177,14 +177,14 @@
    \kappa\rangle
  \\[2ex]
 
- \SEM{\GOTO{g}{C}}{\xi}{\Gamma}{\tau}{\kappa}
+ \SEM{\GOTO{n}{C}}{\xi}{\Gamma}{\tau}{\kappa}
  & = 
- & \langle\xi',\Gamma',\tau\setminus[g],\kappa\setminus[g]\rangle
+ & \langle\xi',\Gamma',\tau\setminus[n],\kappa\setminus[n]\rangle
  \\[1ex]
 
  & & \mathit{where} ~
  \langle \xi', []::\Gamma', []::\tau, []::\kappa\rangle
- = \SEM{C}{\xi}{[g]::\Gamma}{[]::\tau}{[]::\kappa}
+ = \SEM{C}{\xi}{[\OPEN{n}]::\Gamma}{[]::\tau}{[]::\kappa}
  \\[2ex]
 
 \end{array}