aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/newsyntax.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/newsyntax.tex')
-rw-r--r--doc/newsyntax.tex2
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/newsyntax.tex b/doc/newsyntax.tex
index 79d680fcb..f71a22047 100644
--- a/doc/newsyntax.tex
+++ b/doc/newsyntax.tex
@@ -701,4 +701,6 @@ 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).
+Remplacer "Check n" par "n:Check ..."
+
\end{document}