aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-04-02 19:13:58 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-04-09 11:52:17 +0200
commit2ddc9d12bd4616f10245c40bc0c87ae548911809 (patch)
treebd3cea37a3f145510195aaa128ea6fac7f988664 /doc
parent21d308fc083ee395e7b1ff78e75ec3a1305cb2f4 (diff)
Fixing #5420 as well as many related bugs due to miscounting let-ins.
- Supporting let-ins in tactic "fix", and hence in interactive Fixpoint and mutual theorems. - Documenting more precisely the meaning of n in tactic "fix id n". - Fixing computation of recursive index at interpretation time in the presence of let-ins.
Diffstat (limited to 'doc')
-rw-r--r--doc/refman/RefMan-tac.tex6
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 3f1241186..0edc66f83 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -2618,9 +2618,9 @@ as the ones described in Section~\ref{Tac-induction}.
In the syntax of the tactic, the identifier {\ident} is the name given
to the induction hypothesis. The natural number {\num} tells on which
premise of the current goal the induction acts, starting
-from 1 and counting both dependent and non dependent
-products. Especially, the current lemma must be composed of at least
-{\num} products.
+from 1, counting both dependent and non dependent
+products, but skipping local definitions. Especially, the current
+lemma must be composed of at least {\num} products.
Like in a {\tt fix} expression, the induction
hypotheses have to be used on structurally smaller arguments.