diff options
Diffstat (limited to 'doc/refman/RefMan-tac.tex')
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index d23a49bc6..2da12c8d6 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -2289,6 +2289,12 @@ giving \texttt{injection {\term} as} (with an empty list of names). To obtain this behavior, the option {\tt Set Structural Injection} must be activated. This option is off by default. +By default, \texttt{injection} only creates new equalities between +terms whose type is in sort \texttt{Type} or \texttt{Set}, thus +implementing a special behavior for objects that are proofs +of a statement in \texttt{Prop}. This behavior can be turned off +by setting the option \texttt{Set Keep Proof Equalities}. +\optindex{Keep Proof Equalities} \subsection{\tt inversion \ident} \tacindex{inversion} @@ -2308,6 +2314,14 @@ latter is first introduced in the local context using stock the lemmas whenever the same instance needs to be inverted several times. See Section~\ref{Derive-Inversion}. +\Rem Part of the behavior of the \texttt{inversion} tactic is to generate +equalities between expressions that appeared in the hypothesis that is +being processed. By default, no equalities are generated if they relate +two proofs (i.e. equalities between terms whose type is in +sort \texttt{Prop}). This behavior can be turned off by using the option +\texttt{Set Keep Proof Equalities.} +\optindex{Keep Proof Equalities} + \begin{Variants} \item \texttt{inversion \num} |