From 5ea3d1b1e01f56573e72d7818a4b7e6393ffdfa8 Mon Sep 17 00:00:00 2001
From: Théo Winterhalter
Date: Wed, 26 Sep 2018 11:26:50 +0200
Subject: Combined Scheme tests sort to use either "*" or "/\"

And update documentation.---
 doc/sphinx/proof-engine/tactics.rst | 1 +
 1 file changed, 1 insertion(+)

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

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index f99c539251..db9f04ba11 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -2214,6 +2214,7 @@ and an explanation of the underlying technique.
    ``simple inversion``.
 
 .. tacv:: inversion @ident using @ident
+   :name: inversion ... using ...
 
    Let :n:`@ident` have type :g:`(I t)` (:g:`I` an inductive predicate) in the
    local context, and :n:`@ident` be a (dependent) inversion lemma. Then, this
-- 
cgit v1.2.3