aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-11-03 09:34:02 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-11-03 09:34:02 +0000
commitd9e8471056a857325963e481d17803915b1fcfe0 (patch)
treed66c8044d7fa93afdc3f2c7ffa43e0903395aa10
parent0666d4787acb1254144a0b7d36bcc533b5ca8dbc (diff)
Divers
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3201 85f007b7-540e-0410-9357-904b9bb8a0f7
-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}