From e75cd30ff9fc61ce3de31c88645d9bb85128841c Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Thu, 10 May 2012 14:51:33 +0000
Subject: Addedum to documentation of bullets: I now use the dedicated
 coq_example environment to display the example.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15295 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile.common                 | 4 ++--
 doc/refman/RefMan-pro.tex       | 4 ++--
 doc/refman/Reference-Manual.tex | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/Makefile.common b/Makefile.common
index f109ae5738..68eb8de7e3 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -120,14 +120,14 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \
   RefMan-cic.v.tex RefMan-lib.v.tex \
   RefMan-tacex.v.tex RefMan-syn.v.tex \
   RefMan-oth.v.tex RefMan-ltac.v.tex \
-  RefMan-decl.v.tex \
+  RefMan-decl.v.tex RefMan-pro.v.tex \
   Cases.v.tex Coercion.v.tex Extraction.v.tex \
   Program.v.tex Omega.v.tex Micromega.v.tex Polynom.v.tex Nsatz.v.tex \
   Setoid.v.tex Helm.tex Classes.v.tex )
 
 REFMANTEXFILES:=$(addprefix doc/refman/, \
   headers.sty Reference-Manual.tex \
-  RefMan-pre.tex RefMan-int.tex RefMan-pro.tex RefMan-com.tex \
+  RefMan-pre.tex RefMan-int.tex RefMan-com.tex \
   RefMan-uti.tex RefMan-ide.tex RefMan-add.tex RefMan-modr.tex ) \
   $(REFMANCOQTEXFILES) \
 
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index c11c28db87..ca3a9cc985 100644
--- a/doc/refman/RefMan-pro.tex
+++ b/doc/refman/RefMan-pro.tex
@@ -259,7 +259,7 @@ level provided they are delimited by these. Available bullets are
 {\tt -}, {\tt +} and {\tt *} (without a terminating period).
 
 The following example script illustrates all these features:
-\begin{verbatim}
+\begin{coq_example*}
 Goal (((True/\True)/\True)/\True)/\True.
 Proof.
   split.
@@ -272,7 +272,7 @@ Proof.
       * trivial.
     + trivial.
   - trivial.
-\end{verbatim}
+\end{coq_example*}
 
 
 \section{Requesting information}
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index b3cca6f137..4736012e8f 100644
--- a/doc/refman/Reference-Manual.tex
+++ b/doc/refman/Reference-Manual.tex
@@ -88,7 +88,7 @@ Options A and B of the licence are {\em not} elected.}
 
 \part{The proof engine}
 \include{RefMan-oth.v}% Vernacular commands
-\include{RefMan-pro}% Proof handling
+\include{RefMan-pro.v}% Proof handling
 \include{RefMan-tac.v}% Tactics and tacticals
 \include{RefMan-ltac.v}% Writing tactics
 \include{RefMan-tacex.v}% Detailed Examples of tactics
-- 
cgit v1.2.3