Documentation Declare Implicit Tactic, Print Canonical Projections, ... + légère restructuration autour de Proof with et Hint Rewrite + maj crédits

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9030 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 0 deletions

diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index 7af3f64156..0fd6f64d8f 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -267,6 +267,12 @@ applied and $v_i$ is applied to the $i$-th generated subgoal by the
 application of $v_0$, for $=1,...,n$. It fails if the application of
 $v_0$ does not generate exactly $n$ subgoals.
 
+\variant If no tactic is given for the $i$-th generated subgoal, it
+behaves as if the tactic {\tt idtac} were given. For instance, {\tt
+split ; [ | auto ]} is a shortcut for
+{\tt split ; [ idtac | auto ]}.
+
+
 \subsubsection{For loop}
 \tacindex{do}
 \index{Tacticals!do@{\tt do}}