- Fixed bug #2021 (uncaught exception with injection/discriminate when

  the inductive status of a projectable position comes from a
  dependency).
- Improved doc of the stdlib chapter (see bug #2018), and fixed tex
  bugs introduced in r11725.
- Applied wish #2012 (max_dec transparent).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11728 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 3 insertions, 1 deletions

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 89b7350f3..c27a3357e 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -47,7 +47,7 @@
 \newcommand{\Rem}{\medskip \noindent {\bf Remark: }}
 \newcommand{\Rems}{\medskip \noindent {\bf Remarks: }}
 \newcommand{\Example}{\medskip \noindent {\bf Example: }}
-\newcommand{\Examples}{\medskip \noindent {\bf Examples: }}
+\newcommand{\examples}{\medskip \noindent {\bf Examples: }}
 \newcommand{\Warning}{\medskip \noindent {\bf Warning: }}
 \newcommand{\Warns}{\medskip \noindent {\bf Warnings: }}
 \newcounter{ex}
@@ -61,6 +61,8 @@
 \newenvironment{ErrMsgs}{\ErrMsgx\begin{enumerate}}{\end{enumerate}}
 \newenvironment{Remarks}{\Rems\begin{enumerate}}{\end{enumerate}}
 \newenvironment{Warnings}{\Warns\begin{enumerate}}{\end{enumerate}}
+\newenvironment{Examples}{\medskip\noindent{\bf Examples:}
+\begin{enumerate}}{\end{enumerate}}
 
 %\newcommand{\bd}{\noindent\bf}
 %\newcommand{\sbd}{\vspace{8pt}\noindent\bf}