From 33f22b5496af7e1da96a40956a7b7124a1b67032 Mon Sep 17 00:00:00 2001
From: narboux
Date: Mon, 3 May 2004 10:59:24 +0000
Subject: deux questions

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

diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index 83401e2d5d..072b90ff88 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -1564,6 +1564,15 @@ Notation "x $^
 because ``$^2$'' is an iso-latin character. If you really want this kind of notation you should use UTF-8.
 
 
+\Question{Why ``no associativity'' and  ``left associativity'' at the same level does not work ?}
+
+Because we relie on camlp4 for syntactical analysis and camlp4 does not really implement no associativity. By default, non associative operators are defined as right associative.
+
+
+
+\Question{How can I know the associativity associated with a level ?}
+
+You can do ``Print Grammar constr'', and decode the output from camlp4, good luck !
 
 \section{Modules}
 
@@ -1989,6 +1998,16 @@ Opaque definitions can not be unfolded but transparent ones can.
 Sometime you can use the {\abstracttac} tactic, which makes as if you had
 stated some local lemma, this speeds up the typing process.
 
+\Question{Why \texttt{Reset Initial.} does not work when using \texttt{coqc} ?}
+
+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 ``Cannot solve a second-order unification problem'' ?}
 
 You can help {\Coq} using the {\pattern} tactic.
-- 
cgit v1.2.3