diff options
| author | Guillaume Melquiond | 2015-02-05 14:48:03 +0100 |
|---|---|---|
| committer | Guillaume Melquiond | 2015-02-05 16:48:29 +0100 |
| commit | 0e35acf14e0289b5a531d385eaf0506db4430da4 (patch) | |
| tree | 1572f00cfa9f7516e397cc5311d6ccd77ea436c8 /doc/refman/RefMan-oth.tex | |
| parent | 2c0f1eb6f9a6e16b2b4d3a99542df7f49c81f6ea (diff) | |
Fix some documentation typos.
Diffstat (limited to 'doc/refman/RefMan-oth.tex')
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index ce230a0f73..40e0ecc11c 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -308,9 +308,9 @@ statement's conclusion has the form {\tt ({\term} t1 .. tn)}. This command is useful to remind the user of the name of library lemmas. -\begin{coq_example*} +\begin{coq_eval} Reset Initial. -\end{coq_example*} +\end{coq_eval} \begin{coq_example} SearchHead le. |