diff options
| author | Pierre-Marie Pédrot | 2015-01-29 22:40:58 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-01-29 22:40:58 +0100 |
| commit | a340265c9f88df990649481c8ecbe8a513ac4756 (patch) | |
| tree | c9e02defb10bcdb258d75cb6f156657654f65f1f /doc/refman/RefMan-lib.tex | |
| parent | 51b15993cb4a9cc2521b6107b7f4195b21040087 (diff) | |
| parent | db293d185f8deb091d4b086f327caa0f376d67d7 (diff) | |
Merge branch 'v8.5'
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 49382f3e20..7227f4b7b6 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. |