From 29c67f1d97221755415ace1e4317cb7af92e24f3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 29 May 2002 11:10:24 +0000
Subject: 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
---
 doc/newsyntax.tex | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'doc')

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}
-- 
cgit v1.2.3