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 0680231a85ef725abfb8b96e430c33cbd76650bd..19c136f2a6aac3f82b62caf4cd06c77c3367bec5 100644 (file)
--- 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)