From 8aeaf2d184f95037021a644cf03e7ae340d8c790 Mon Sep 17 00:00:00 2001
From: Clément Pit-Claudel
Date: Thu, 16 May 2019 11:00:19 -0400
Subject: [refman] Document etransitivity

---
 doc/sphinx/proof-engine/tactics.rst | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'doc/sphinx/proof-engine')

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
 ---------------------------
-- 
cgit v1.2.3