From 2b61cb974c847669eaf24dfbf47d8615812481fb Mon Sep 17 00:00:00 2001
From: barras
Date: Sat, 11 Oct 2003 00:20:33 +0000
Subject: mise a jour nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4595 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/syntax-v8.tex | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'doc')

diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex
index c4da450653..b947a033a4 100644
--- a/doc/syntax-v8.tex
+++ b/doc/syntax-v8.tex
@@ -313,6 +313,7 @@ $$
 \text{Symbol} & \text{precedence} \\
 \hline
 \infx{,}             & 250L \\
+\KWD{IF}~\notv~\KWD{then}~\notv~\KWD{else}~\notv & 200 \\
 \infx{:}             & 100R \\
 \infx{\rightarrow}\quad \infx{\leftrightarrow}  & 80R \\
 \infx{\vee}          & 70R \\
@@ -355,8 +356,7 @@ $$
 \end{array}
 $$
 
-
-%% ``IF then else'' is missing
+%% Strange: nat + {x:nat|x=x} * nat  == ( + ) *
 
 \section{Grammar of tactics}
 
-- 
cgit v1.2.3