From 68b36b3a564c17ca59443fb772cce9c5d82b1a1f Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 26 Oct 2005 11:52:37 +0000
Subject: [PATCH] added constraing on non-empty context for tactic application

---
 helm/ocaml/tactics/doc/main.tex | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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)
-- 
2.39.2