From 8a02eb5664b115d8afcf3b92c50a402f3bf402e6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 11 Oct 2004 10:22:02 +0000
Subject: Ajout pr�vention �chec en pr�sence de sous-typage

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

diff --git a/doc/RefMan-ext.tex b/doc/RefMan-ext.tex
index f52e1cf2ee..503d7571d6 100644
--- a/doc/RefMan-ext.tex
+++ b/doc/RefMan-ext.tex
@@ -1011,6 +1011,24 @@ Conversely, to restore the hidding of implicit arguments, use command
 
 \SeeAlso {\tt Set Printing All} in section \ref{SetPrintingAll}.
 
+\subsection{Interaction with subtyping}
+
+When an implicit argument can be inferred from the type of more than
+one of the other arguments, then only the type of the first of these
+arguments is taken into account, and not an upper type of all of
+them.  As a consequence, the inference of the implicit argument of
+``='' fails in
+
+\begin{coq_example*}
+Check nat = Prop.
+\end{coq_example*}
+
+but succeeds in 
+
+\begin{coq_example*}
+Check Prop = nat.
+\end{coq_example*}
+
 \subsection{Canonical structures
 \comindex{Canonical Structure}}
 
-- 
cgit v1.2.3