]> matita.cs.unibo.it Git - helm.git/commitdiff
added constraing on non-empty context for tactic application
authorStefano Zacchiroli <zack@upsilon.cc>
Wed, 26 Oct 2005 11:52:37 +0000 (11:52 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Wed, 26 Oct 2005 11:52:37 +0000 (11:52 +0000)
helm/ocaml/tactics/doc/main.tex

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