From 6f23cba6d691e149e62f36b46eb4c58ef6a826c8 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Sun, 25 Mar 2018 18:24:49 +0200 Subject: Clarify wording in tactics documentation. Closes #6980. --- doc/sphinx/proof-engine/tactics.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index da34e3b55..2af73c28e 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1635,7 +1635,7 @@ analysis on inductive or co-inductive objects (see :ref:`TODO-4.5`). .. tacv:: elim @term using @term .. tacv:: elim @term using @term with @bindings_list - Allows the user to give explicitly an elimination predicate :n:`@term` that + Allows the user to give explicitly an induction principle :n:`@term` that is not the standard one for the underlying inductive type of :n:`@term`. The :n:`@bindings_list` clause allows instantiating premises of the type of :n:`@term`. -- cgit v1.2.3