diff options
Diffstat (limited to 'doc/RefMan-lib.tex')
| -rwxr-xr-x | doc/RefMan-lib.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/RefMan-lib.tex b/doc/RefMan-lib.tex index 1a6aa2dab3..757a0e2ce5 100755 --- a/doc/RefMan-lib.tex +++ b/doc/RefMan-lib.tex @@ -541,7 +541,7 @@ provides a scope {\tt nat\_scope} gathering standard notations for common operations (+,*) and a decimal notation for numbers. That is he can write \texttt{3} for \texttt{(S (S (S O)))}. This also works on the left hand side of a \texttt{match} expression (see for example -section \ref{Refine-example}). This scope is opened by default. +section~\ref{refine-example}). This scope is opened by default. %Remove the redefinition of nat \begin{coq_eval} |