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') diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 9873a541a..b79d28138 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