diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/newsyntax.tex | 6 |
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} |