From d87d8c6e694037762082a213d443e8225f96ad8a Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 25 Jul 2014 12:38:42 +0200
Subject: Warns about inconsistency of generated name in evars and goals.

See bug #1041
---
 doc/refman/RefMan-tac.tex | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index b79d281381..bee91c952f 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -1341,6 +1341,11 @@ existential variable from right to left in the conclusion. This cannot be
 the number of the existential variable since this number is different
 in every session.
 
+When you are refering to hypotheses which you did not name
+explicitely, be aware that Coq may make a different decision on how to
+name the variable in the current goal and in the context of the
+existential variable. This can lead to surprising behaviours.
+
 \begin{Variants}
   \item {\tt instantiate ( {\num} := {\term} ) in \ident}
 
-- 
cgit v1.2.3