Warns about inconsistency of generated name in evars and goals.

See bug #1041

1 files changed, 5 insertions, 0 deletions

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}