Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et commandes vernaculaires (cf dev/changements.txt pour plus de précisions)

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

1 files changed, 6 insertions, 0 deletions

diff --git a/doc/newsyntax.tex b/doc/newsyntax.tex
index eb005520d3..035d3d8bd2 100644
--- a/doc/newsyntax.tex
+++ b/doc/newsyntax.tex
@@ -676,4 +676,10 @@ Remplacer Save. par Qed.
 
 Remplacer Implicit Arguments On/Off par Set/Unset Implicit Arguments.
 
+La syntaxe \verb=Intros (a,b)= est inutile, \verb=Intros [a b]= fait l'affaire.
+
+Mettre des \verb=?x= plutot que des \verb=?1= dans les motifs de ltac ??
+
+Virer \verb=Goal= sans argument (synonyme de \verb=Proof= et sans effets).
+
 \end{document}