diff options
| author | Pierre-Marie Pédrot | 2015-01-29 22:40:58 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-01-29 22:40:58 +0100 |
| commit | a340265c9f88df990649481c8ecbe8a513ac4756 (patch) | |
| tree | c9e02defb10bcdb258d75cb6f156657654f65f1f /doc/refman/RefMan-oth.tex | |
| parent | 51b15993cb4a9cc2521b6107b7f4195b21040087 (diff) | |
| parent | db293d185f8deb091d4b086f327caa0f376d67d7 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'doc/refman/RefMan-oth.tex')
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 5 |
1 files changed, 3 insertions, 2 deletions
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} |