diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-04-04 23:06:00 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-04-04 23:06:12 +0200 |
| commit | 213251134eb56625e4b8cff2879d00cd8cc7ec6a (patch) | |
| tree | 5695c7a1c355f8c4f9f34902a02e260032722b00 | |
| parent | a324162435df4666be99a3872717c84d93cca5ce (diff) | |
Fix for bug #3107.
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 7b09d8463..9873a541a 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3020,7 +3020,7 @@ After that command, the expression {\tt (minus (S x) y)} is left untouched by A special heuristic to determine if a constant has to be unfolded can be activated with the following command: \begin{coq_example*} -Arguments minus x y : simpl nomatch +Arguments minus x y : simpl nomatch. \end{coq_example*} The heuristic avoids to perform a simplification step that would expose a {\tt match} construct in head position. For example the @@ -3272,6 +3272,9 @@ against the hints rather than pattern-matching {\tt apply}). As a consequence, {\tt eauto} can solve such a goal: +\begin{coq_eval} +Reset Initial. +\end{coq_eval} \begin{coq_example} Hint Resolve ex_intro. Goal forall P:nat -> Prop, P 0 -> exists n, P n. |