From be01deca2b8ff22505adaa66f55f005673bf2d85 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 31 May 2014 15:06:46 +0200
Subject: More on injection over a projectable "existT". - Fixing syntax
 "injection ... as ..." which was not working. - Now applying the
 simplification on any "existT" generated by "injection" (possible source of
 incompatibilities).

---
 doc/refman/RefMan-tac.tex | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

(limited to 'doc/refman/RefMan-tac.tex')

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 9873a541ac..b79d281381 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2096,14 +2096,13 @@ injection H0.
 Abort.
 \end{coq_eval}
 
-Beware that \texttt{injection} yields always an equality in a sigma type
-whenever the injected object has a dependent type.
-
-\Rem There is a special case for dependent pairs. If we have a decidable
-equality over the type of the first argument, then it is safe to do
-the projection on the second one, and so {\tt injection} will work fine.
-To define such an equality, you have to use the {\tt Scheme} command
-(see \ref{Scheme}).
+Beware that \texttt{injection} yields an equality in a sigma type
+whenever the injected object has a dependent type $P$ with its two
+instances in different types $(P~t_1~...~t_n)$ and
+$(P~u_1~...~u_n)$. If $t_1$ and $u_1$ are the same and have for type
+an inductive type for which a decidable equality has been declared
+using the command {\tt Scheme Equality} (see \ref{Scheme}), the use of
+a sigma type is avoided.
 
 \Rem If some quantified hypothesis of the goal is named {\ident}, then
 {\tt injection {\ident}} first introduces the hypothesis in the local
-- 
cgit v1.2.3

