From 2f66d100ba43d7afcfd7fdc41fd46d5e5df65f24 Mon Sep 17 00:00:00 2001
From: narboux
Date: Wed, 19 May 2004 09:06:07 +0000
Subject: ajout question implicit

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

diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex
index c91b6b25bd..701e4fd260 100644
--- a/doc/newfaq/main.tex
+++ b/doc/newfaq/main.tex
@@ -1277,6 +1277,19 @@ is rendered into something like
 Otherwise said, {\generalize} is not rendered in a forward-reasoning way,
 while {\assert} is.
 
+\Question{What can I do if \Coq can not infer some implicit argument ?}
+
+You can state explicitely what this implicit argument is. See \ref{implicit}.
+
+\Question{How can I explicit some implicit argument ?}\label{implicit}
+
+Just use \texttt{A:=term} where \texttt{A} is the argument.
+
+For instance if you want to use the existence of ``nil'' on nat*nat lists:
+\begin{verbatim}
+exists (nil (A:=(nat*nat))).
+\end{verbatim}
+
 \Question{Is there anyway to do pattern matching with dependent types?}
 
 todo
-- 
cgit v1.2.3