- 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

1 files changed, 3 insertions, 3 deletions

diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index be5980fe4..89b7350f3 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}}