From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 26 Oct 2005 11:52:37 +0000 (+0000)
Subject: added constraing on non-empty context for tactic application
X-Git-Tag: V_0_7_2_3~180
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=68b36b3a564c17ca59443fb772cce9c5d82b1a1f;p=helm.git

added constraing on non-empty context for tactic application
---

diff --git a/helm/ocaml/tactics/doc/main.tex b/helm/ocaml/tactics/doc/main.tex
index 0680231a8..19c136f2a 100644
--- a/helm/ocaml/tactics/doc/main.tex
+++ b/helm/ocaml/tactics/doc/main.tex
@@ -197,7 +197,9 @@
    :: \DEEPCLOSE(G^c_n,S)
    \rangle
  \\[1ex]
- \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{where} ~
+ \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{where} ~ n\geq 1}
+ \\[1ex]
+ \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{and} ~
   \Gamma' = \ZEROPOS(G^o_n)
   \land \tau' = \REMOVEGOALS(G^c_n,\tau)
   \land \kappa' = \REMOVEGOALS(G^o_n,\kappa)