diff options
Diffstat (limited to 'doc/newsyntax.tex')
| -rw-r--r-- | doc/newsyntax.tex | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/newsyntax.tex b/doc/newsyntax.tex index a8622445f..ea4b8c59a 100644 --- a/doc/newsyntax.tex +++ b/doc/newsyntax.tex @@ -707,6 +707,8 @@ l'ajouter à côté des Require Ring. \item Remplacer AddPath par Add LoadPath (ou + court) +\item Unify + and \{\}+\{\} and +\{\} using Prop $\leq$ Set ?? + \item Remplacer Implicit Arguments On/Off par Set/Unset Implicit Arguments. \item La syntaxe \verb=Intros (a,b)= est inutile, \verb=Intros [a b]= fait l'affaire. |