From 0d2e40ca62568ec9206bf71356770199a237d37e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 3 Aug 2004 21:49:18 +0000
Subject: Probl�mes hevea + question evars

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8583 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/newfaq/main.tex | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index e68d1e0fd4..c1121d5884 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -14,6 +14,10 @@
 
 %\input{../macros.tex}
 
+% Making hevea happy
+%HEVEA \renewcommand{\textbar}{|}
+%HEVEA \renewcommand{\textunderscore}{\_}
+
 \def\Question#1{\stepcounter{question}\subsubsection{#1}}
 
 % version et date
@@ -2204,9 +2208,12 @@ The initial state corresponds to the state of coqtop when the interactive
 session began. It does not make sense in files to compile.
 
 
-\Question{What can I do if I get ``(*No more subgoals but non-instantiated existential variables*)''?}
-
+\Question{What can I do if I get ``No more subgoals but non-instantiated existential variables''?}
 
+This means that {\eauto} or {\eapply} didn't instantiate an
+existential variable which eventually got erased by some computation.
+You have to backtrack to the faulty occurrence of {\eauto} or
+{\eapply} and give the missing argument an explicit value.
 
 \Question{What can I do if I get ``Cannot solve a second-order unification problem''?}
 
-- 
cgit v1.2.3