diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-01-29 15:27:49 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-01-29 15:27:49 +0100 |
| commit | 1dfcae672aa1630bb1fe841bae9321dd9f221fc4 (patch) | |
| tree | 7346de43dab635ed8d3616b8e7cdf70f9e2ff757 /doc/refman/RefMan-lib.tex | |
| parent | fe038eea4f1c62a209db18fadb69dbab80e16c16 (diff) | |
Remove spurious "Loading ML file" and "<W> Grammar extension" from the reference manual.
Diffstat (limited to 'doc/refman/RefMan-lib.tex')
| -rw-r--r-- | doc/refman/RefMan-lib.tex | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/doc/refman/RefMan-lib.tex b/doc/refman/RefMan-lib.tex index 49382f3e2..7227f4b7b 100644 --- a/doc/refman/RefMan-lib.tex +++ b/doc/refman/RefMan-lib.tex @@ -892,8 +892,10 @@ Figure~\ref{zarith-syntax} shows the notations provided by {\tt Z\_scope}. It specifies how notations are interpreted and, when not already reserved, the precedence and associativity. -\begin{coq_example} +\begin{coq_example*} Require Import ZArith. +\end{coq_example*} +\begin{coq_example} Check (2 + 3)%Z. Open Scope Z_scope. Check 2 + 3. @@ -968,8 +970,10 @@ Notation & Interpretation \\ \begin{coq_eval} Reset Initial. \end{coq_eval} -\begin{coq_example} +\begin{coq_example*} Require Import Reals. +\end{coq_example*} +\begin{coq_example} Check (2 + 3)%R. Open Scope R_scope. Check 2 + 3. |