From b18a6d179903546cbf5745e601ab221f06e30078 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 29 Dec 2008 17:15:52 +0000
Subject: - Added support for subterm matching in SearchAbout. - Backtrack on
 precise unfolding of "iff" in "tauto": it has effects on   the naming of
 hypotheses (especially when doing "case H" with H of   type "{x|P<->Q}" since
 not unfolding will eventually introduce a name   "i" while unfolding will
 eventually introduce a name "a" (deep sigh). - Miscellaneous (error when a
 plugin is missing, doc hnf, standardization   of names manipulating type
 constr_pattern, ...).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11725 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/common/macros.tex | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc/common')

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index be5980fe43..89b7350f3a 100755
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -47,6 +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{\Warning}{\medskip \noindent {\bf Warning: }}
 \newcommand{\Warns}{\medskip \noindent {\bf Warnings: }}
 \newcounter{ex}
@@ -60,8 +61,6 @@
 \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}
@@ -191,11 +190,12 @@
 \newcommand{\nestedpattern}{\nterm{nested\_pattern}}
 \newcommand{\name}{\nterm{name}}
 \newcommand{\num}{\nterm{num}}
-\newcommand{\pattern}{\nterm{pattern}}
+\newcommand{\pattern}{\nterm{pattern}} % pattern for pattern-matching
 \newcommand{\orpattern}{\nterm{or\_pattern}}
 \newcommand{\intropattern}{\nterm{intro\_pattern}}
 \newcommand{\disjconjintropattern}{\nterm{disj\_conj\_intro\_pattern}}
 \newcommand{\namingintropattern}{\nterm{naming\_intro\_pattern}}
+\newcommand{\termpattern}{\nterm{term\_pattern}} % term with holes
 \newcommand{\pat}{\nterm{pat}}
 \newcommand{\pgs}{\nterm{pgms}}
 \newcommand{\pg}{\nterm{pgm}}
-- 
cgit v1.2.3