From 9e04031196175111302681d96d975804bd7e1850 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 9 Jul 2012 18:18:01 +0000
Subject: The tactic remember now accepts a final eqn:H option (grant wish
 #2489)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15567 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/refman/RefMan-tac.tex | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'doc')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 505db64d08..124036afa9 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -626,6 +626,11 @@ Section~\ref{Occurrences clauses}.
   This behaves as {\tt set (} {\ident} := {\term} {\tt ) in *} and using a
   logical (Leibniz's) equality instead of a local definition.
 
+\item {\tt remember {\term} {\tt as} {\ident} {\tt eqn:\ident}}
+
+  This behaves as {\tt remember {\term} {\tt as} {\ident}}, except
+  that the name of the generated equality is also given.
+
 \item {\tt remember {\term} {\tt as} {\ident} in {\occgoalset}}
 
   This is a more general form of {\tt remember} that remembers the
-- 
cgit v1.2.3