diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-05-08 18:11:43 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-05-08 20:44:29 +0200 |
commit | 5ad72416fc614c8c876d80673d7a7c2e6f33b9e4 (patch) | |
tree | b6f4dda0db9a2c82f7da06c2ee74d84d576ced9a | |
parent | e1e750683d52e7d2b63a707b62c4d2af0e01a532 (diff) |
Typo reference manual
-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} |