From 1dfcae672aa1630bb1fe841bae9321dd9f221fc4 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Thu, 29 Jan 2015 15:27:49 +0100
Subject: Remove spurious "Loading ML file" and "<W> Grammar extension" from
 the reference manual.

---
 doc/refman/RefMan-lib.tex | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'doc/refman/RefMan-lib.tex')

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.
-- 
cgit v1.2.3

