diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/proofs/writing-proofs/rewriting.rst | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index 2de6b2a18c..b7f2927000 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -146,6 +146,13 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. only in the conclusion of the goal. The clause argument must not contain any ``type of`` nor ``value of``. + .. tacv:: cutrewrite {? {| <- | -> } } (@term__1 = @term__2) {? in @ident } + :name: cutrewrite + + .. deprecated:: 8.5 + + Use :tacn:`replace` instead. + .. tacn:: subst @ident :name: subst |