From: Stefano Zacchiroli Date: Fri, 30 Sep 2005 14:00:33 +0000 (+0000) Subject: fixed some typos X-Git-Tag: V_0_7_2_3~272 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f0f2ae23475a8e7b1372fdd75a0e4856fb468c19;p=helm.git fixed some typos --- diff --git a/helm/ocaml/tactics/doc/main.tex b/helm/ocaml/tactics/doc/main.tex index 43e17ebe8..b2996c116 100644 --- 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}