diff options
| author | Clément Pit-Claudel | 2019-05-16 11:00:19 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-05-19 19:19:30 -0400 |
| commit | 8aeaf2d184f95037021a644cf03e7ae340d8c790 (patch) | |
| tree | cf07ebb417bc5f44d4379716fb8fdb2b3a5fc040 /doc/sphinx/proof-engine | |
| parent | 4a69c594b484cb7e9af28b8ba9608a228e2376f1 (diff) | |
[refman] Document etransitivity
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 4297e5a64b..4e47621938 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -4400,6 +4400,11 @@ Equality This tactic applies to a goal that has the form :g:`t=u` and transforms it into the two subgoals :n:`t=@term` and :n:`@term=u`. + .. tacv:: etransitivity + + This tactic behaves like :tacn:`transitivity`, using a fresh evar instead of + a concrete :token:`term`. + Equality and inductive sets --------------------------- |