From 213251134eb56625e4b8cff2879d00cd8cc7ec6a Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Fri, 4 Apr 2014 23:06:00 +0200
Subject: Fix for bug #3107.

---
 doc/refman/RefMan-tac.tex | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'doc/refman')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 7b09d84637..9873a541ac 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.
-- 
cgit v1.2.3