diff options
| author | Théo Zimmermann | 2020-04-22 15:58:44 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2020-04-23 15:15:30 +0200 |
| commit | 14e5c34b9a1ec02f9d1a3107f85ae73834b9045a (patch) | |
| tree | f667e3c10061514611d129835c847a853dcc8087 /doc/sphinx/proof-engine | |
| parent | 3ee19d5722cd6e4a11a8d4c77ce5117bbc3de44a (diff) | |
[refman] Fix name of tactic: function induction -> functional induction.
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 |