diff options
| author | Maxime Dénès | 2016-10-03 11:09:03 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-10-03 11:13:40 +0200 |
| commit | a35a3fd5cf59e262e814afd530ffdc35f085c01d (patch) | |
| tree | 87a13102f6145c238b0696313ceb722beff09f00 /doc | |
| parent | 24d5448c65ba05072a5ab4180c9be95670ce126d (diff) | |
| parent | 0746578040e738d079bcc3289857bb99983a7a22 (diff) | |
Merge remote-tracking branch 'github/pr/304' into v8.6
Was PR#304: fixing bug 4609
Diffstat (limited to 'doc')
| -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 d23a49bc67..2da12c8d69 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} |