diff options
| author | Hugo Herbelin | 2016-06-29 10:30:17 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-29 12:46:54 +0200 |
| commit | 5c91ebc9b995355a5a1f9713be8b9fc74d3ba242 (patch) | |
| tree | afda8f8f4fc6febe9d986c79e92527e98554d071 | |
| parent | cbf100f49880284383d8c3cc8c1a35021d6a2a0c (diff) | |
Updated CHANGES about subst. More on recursive equations in reference manual.
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 3 |
2 files changed, 4 insertions, 0 deletions
@@ -13,6 +13,7 @@ Specification language Tactics - Flag "Bracketing Last Introduction Pattern" is now on by default. +- Flag "Regular Subst Tactic" is now on by default. - New flag "Shrink Abstract" that minimalizes proofs generated by the abstract tactical w.r.t. variables appearing in the body of the proof. On by default and deprecated. Minor source of incompatibility diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index c4ea1f5f9c..2d9cc12fd7 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -2872,6 +2872,9 @@ activated, {\tt subst} also deals with the following corner cases: subst} would be necessary to replace {\ident$_2$} by $t$ or $t'$ respectively. +\item The presence of a recursive equation which without the option + would be a cause of failure of {\tt subst}. + \item A context with cyclic dependencies as with hypotheses {\tt \ident$_1$ = f~\ident$_2$} and {\tt \ident$_2$ = g~\ident$_1$} which without the option would be a cause of failure of {\tt subst}. |