diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/Natural.tex | 6 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 10 |
2 files changed, 8 insertions, 8 deletions
diff --git a/doc/refman/Natural.tex b/doc/refman/Natural.tex index 69dfab87c6..9a9abe5dff 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} diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 769927cafa..f6e44f91ab 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -424,7 +424,7 @@ The default is to not print synthesisable types. \subsubsection{Printing matching on irrefutable pattern \comindex{Add Printing Let {\ident}} \comindex{Remove Printing Let {\ident}} -\comindex{Test Printing Let {\ident}} +\comindex{Test Printing Let for {\ident}} \comindex{Print Table Printing Let}} If an inductive type has just one constructor, @@ -443,7 +443,7 @@ pattern-matching is written using a {\tt let} expression. This removes {\ident} from this list. \begin{quote} -{\tt Test Printing Let {\ident}.} +{\tt Test Printing Let for {\ident}.} \end{quote} This tells if {\ident} belongs to the list. @@ -460,7 +460,7 @@ it is sensible to the command {\tt Reset}. \subsubsection{Printing matching on booleans \comindex{Add Printing If {\ident}} \comindex{Remove Printing If {\ident}} -\comindex{Test Printing If {\ident}} +\comindex{Test Printing If for {\ident}} \comindex{Print Table Printing If}} If an inductive type is isomorphic to the boolean type, @@ -479,7 +479,7 @@ pattern-matching is written using an {\tt if} expression. This removes {\ident} from this list. \begin{quote} -{\tt Test Printing If {\ident}.} +{\tt Test Printing If for {\ident}.} \end{quote} This tells if {\ident} belongs to the list. @@ -498,7 +498,7 @@ it is sensible to the command {\tt Reset}. This example emphasizes what the printing options offer. \begin{coq_example} -Test Printing Let prod. +Test Printing Let for prod. Print fst. Remove Printing Let prod. Unset Printing Synth. |