diff options
Diffstat (limited to 'doc/refman/RefMan-tacex.tex')
| -rw-r--r-- | doc/refman/RefMan-tacex.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex index 463e2b81a..6667fd5a4 100644 --- a/doc/refman/RefMan-tacex.tex +++ b/doc/refman/RefMan-tacex.tex @@ -64,7 +64,7 @@ induction H. As the hypothesis itself did not appear in the goal, we did not need to use an heterogeneous equality to relate the new hypothesis to the old -one (which just disappeared here). However, the tactic works just a well +one (which just disappeared here). However, the tactic works just as well in this case, e.g.: \begin{coq_eval} |