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-oth.tex | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

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

diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex
index 64fab055ea..ce230a0f73 100644
--- a/doc/refman/RefMan-oth.tex
+++ b/doc/refman/RefMan-oth.tex
@@ -355,8 +355,10 @@ is a variant of {\tt Search
 statements whose conclusion has exactly the expected form, or whose
 statement finishes by the given series of hypothesis/conclusion.
 
-\begin{coq_example}
+\begin{coq_example*}
 Require Import Arith.
+\end{coq_example*}
+\begin{coq_example}
 SearchPattern (_ + _ = _ + _).
 SearchPattern (nat -> bool).
 SearchPattern (forall l : list _, _ l l).
@@ -367,7 +369,6 @@ must occur in two places by using pattern variables `{\texttt
 ?{\ident}}''.
 
 \begin{coq_example}
-Require Import Arith.
 SearchPattern (?X1 + _ = _ + ?X1).
 \end{coq_example}
 
-- 
cgit v1.2.3