Skip to content

Commit

Permalink
Typo reference manual
Browse files Browse the repository at this point in the history
  • Loading branch information
herbelin committed May 8, 2014
1 parent e1e7506 commit 5ad7241
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion doc/refman/RefMan-tacex.tex
Original file line number Diff line number Diff line change
Expand Up @@ -64,7 +64,7 @@

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}
Expand Down

0 comments on commit 5ad7241

Please sign in to comment.