diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 12 |
1 files changed, 3 insertions, 9 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 44f7916cf0..f57f9ff9c9 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -2099,15 +2099,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) See also the larger example of :tacn:`dependent induction` and an explanation of the underlying technique. -.. seealso:: :tacn:`function induction` - -.. tacv:: functional induction (@qualid {+ @term}) as @simple_intropattern using @term with @bindings_list - - Similarly to :tacn:`induction` and :tacn:`elim`, this allows giving - explicitly the name of the introduced variables, the induction principle, and - the values of dependent premises of the elimination scheme, including - *predicates* for mutual induction when :n:`@qualid` is part of a mutually - recursive definition. +.. seealso:: :tacn:`functional induction` .. tacn:: discriminate @term :name: discriminate @@ -2614,6 +2606,8 @@ and an explanation of the underlying technique. assumption. Qed. +.. seealso:: :tacn:`functional inversion` + .. tacn:: fix @ident @num :name: fix |