diff options
Diffstat (limited to 'doc/refman/Natural.tex')
| -rw-r--r-- | doc/refman/Natural.tex | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/refman/Natural.tex b/doc/refman/Natural.tex index 69dfab87c..9a9abe5df 100644 --- a/doc/refman/Natural.tex +++ b/doc/refman/Natural.tex @@ -121,7 +121,7 @@ declared as implicit, type \comindex{Test Natural} \begin{coq_example*} -Test Natural Implicit lem1. +Test Natural Implicit for lem1. \end{coq_example*} \subsubsection*{Implicit proof constructors} @@ -211,7 +211,7 @@ By default, the data type \verb=nat= and the inductive connectives As above, you can remove or test a constant declared implicit. Use {\tt Remove Natural Contractible $id$} or {\tt Test Natural -Contractible $id$}. +Contractible for $id$}. \asubsection{Contractible proof steps} @@ -328,7 +328,7 @@ a non inductive transparent definition. As for implicit and contractible definitions, you can remove or test a non inductive definition declared transparent. Use \texttt{Remove Natural Transparent} \ident or -\texttt{Test Natural Transparent} \ident. +\texttt{Test Natural Transparent for} \ident. \subsubsection*{Transparent inductive definitions} |