mise a jour nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4595 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 53 insertions, 26 deletions

diff --git a/.depend.newcoq b/.depend.newcoq
index 87bfd49f9..c975b9805 100644
--- a/.depend.newcoq
+++ b/.depend.newcoq
@@ -57,7 +57,7 @@ newtheories/Init/Datatypes.vo: newtheories/Init/Datatypes.v newtheories/Init/Not
 newtheories/Init/Peano.vo: newtheories/Init/Peano.v newtheories/Init/Notations.vo newtheories/Init/Datatypes.vo newtheories/Init/Logic.vo
 newtheories/Init/Logic.vo: newtheories/Init/Logic.v newtheories/Init/Notations.vo newtheories/Init/Datatypes.vo
 newtheories/Init/Specif.vo: newtheories/Init/Specif.v newtheories/Init/Notations.vo newtheories/Init/Datatypes.vo newtheories/Init/Logic.vo
-newtheories/Init/Logic_Type.vo: newtheories/Init/Logic_Type.v newtheories/Init/Notations.vo newtheories/Init/Logic.vo
+newtheories/Init/Logic_Type.vo: newtheories/Init/Logic_Type.v newtheories/Init/Datatypes.vo newtheories/Init/Logic.vo
 newtheories/Init/Wf.vo: newtheories/Init/Wf.v newtheories/Init/Notations.vo newtheories/Init/Logic.vo newtheories/Init/Datatypes.vo
 newtheories/Init/Prelude.vo: newtheories/Init/Prelude.v newtheories/Init/Notations.vo newtheories/Init/Datatypes.vo newtheories/Init/Logic.vo newtheories/Init/Specif.vo newtheories/Init/Peano.vo newtheories/Init/Wf.vo
 newtheories/Init/Notations.vo: newtheories/Init/Notations.v
@@ -65,7 +65,7 @@ newtheories/Init/Datatypes.vo: newtheories/Init/Datatypes.v newtheories/Init/Not
 newtheories/Init/Peano.vo: newtheories/Init/Peano.v newtheories/Init/Notations.vo newtheories/Init/Datatypes.vo newtheories/Init/Logic.vo
 newtheories/Init/Logic.vo: newtheories/Init/Logic.v newtheories/Init/Notations.vo newtheories/Init/Datatypes.vo
 newtheories/Init/Specif.vo: newtheories/Init/Specif.v newtheories/Init/Notations.vo newtheories/Init/Datatypes.vo newtheories/Init/Logic.vo
-newtheories/Init/Logic_Type.vo: newtheories/Init/Logic_Type.v newtheories/Init/Notations.vo newtheories/Init/Logic.vo
+newtheories/Init/Logic_Type.vo: newtheories/Init/Logic_Type.v newtheories/Init/Datatypes.vo newtheories/Init/Logic.vo
 newtheories/Init/Wf.vo: newtheories/Init/Wf.v newtheories/Init/Notations.vo newtheories/Init/Logic.vo newtheories/Init/Datatypes.vo
 newtheories/Init/Prelude.vo: newtheories/Init/Prelude.v newtheories/Init/Notations.vo newtheories/Init/Datatypes.vo newtheories/Init/Logic.vo newtheories/Init/Specif.vo newtheories/Init/Peano.vo newtheories/Init/Wf.vo
 newtheories/Logic/Hurkens.vo: newtheories/Logic/Hurkens.v
diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex
index c4da45065..b947a033a 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}
 
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index ce45d73b0..9a9cf9a59 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -109,11 +109,17 @@ let rec mkCLambdaN loc bll c =
 let lpar_id_coloneq =
   Gram.Entry.of_parser "test_lpar_id_coloneq"
     (fun strm ->
-      match Stream.npeek 3 strm with
-	| [("","("); ("IDENT",s); ("", ":=")] ->
-            Stream.junk strm; Stream.junk strm; Stream.junk strm;
-            Names.id_of_string s
-	| _ -> raise Stream.Failure);;
+      match Stream.npeek 1 strm with
+        | [("","(")] ->
+            (match Stream.npeek 2 strm with
+	      | [_; ("IDENT",s)] ->
+                  (match Stream.npeek 3 strm with
+                    | [_; _; ("", ":=")] ->
+                        Stream.junk strm; Stream.junk strm; Stream.junk strm;
+                        Names.id_of_string s
+	            | _ -> raise Stream.Failure)
+              | _ -> raise Stream.Failure)
+        | _ -> raise Stream.Failure)
 
 
 if not !Options.v7 then
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index b03aaf868..fa9a402eb 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -27,28 +27,46 @@ let _ =
 let lpar_id_coloneq =
   Gram.Entry.of_parser "lpar_id_coloneq"
     (fun strm ->
-      match Stream.npeek 3 strm with
-	| [("","("); ("IDENT",s); ("", ":=")] ->
-            Stream.junk strm; Stream.junk strm; Stream.junk strm;
-            Names.id_of_string s
+      match Stream.npeek 1 strm with
+        | [("","(")] ->
+            (match Stream.npeek 2 strm with
+              | [_; ("IDENT",s)] ->
+                  (match Stream.npeek 3 strm with
+	            | [_; _; ("", ":=")] ->
+                        Stream.junk strm; Stream.junk strm; Stream.junk strm;
+                        Names.id_of_string s
+	            | _ -> raise Stream.Failure)
+	      | _ -> raise Stream.Failure)
 	| _ -> raise Stream.Failure)
 
 (* idem for (x:=t) and (1:=t) *)
 let test_lpar_idnum_coloneq =
   Gram.Entry.of_parser "test_lpar_idnum_coloneq"
     (fun strm ->
-      match Stream.npeek 3 strm with
-        | [("","("); (("IDENT"|"INT"),_); ("", ":=")] -> ()
+      match Stream.npeek 1 strm with
+        | [("","(")] ->
+            (match Stream.npeek 2 strm with
+              | [_; (("IDENT"|"INT"),_)] ->
+                  (match Stream.npeek 3 strm with
+                    | [_; _; ("", ":=")] -> ()
+                    | _ -> raise Stream.Failure)
+              | _ -> raise Stream.Failure)
         | _ -> raise Stream.Failure)
 
 (* idem for (x:t) *)
 let lpar_id_colon =
   Gram.Entry.of_parser "test_lpar_id_colon"
     (fun strm ->
-      match Stream.npeek 3 strm with
-        | [("","("); ("IDENT",id); ("", ":")] ->
-            Stream.junk strm; Stream.junk strm; Stream.junk strm;
-            Names.id_of_string id
+      match Stream.npeek 1 strm with
+        | [("","(")] ->
+            (match Stream.npeek 2 strm with
+              | [_; ("IDENT",id)] ->
+                  (match Stream.npeek 3 strm with
+                    | [_; _; ("", ":")] ->
+                        Stream.junk strm; Stream.junk strm; Stream.junk strm;
+                        Names.id_of_string id
+                    | _ -> raise Stream.Failure)
+              | _ -> raise Stream.Failure)
         | _ -> raise Stream.Failure)
 
 (* open grammar entries, possibly in quotified form *)
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 6abbfa9f8..469a9d4bf 100755
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -123,28 +123,28 @@ Definition all := [A:Type][P:A->Prop](x:A)(P x).
 V7only [ Notation Ex  := (ex ?). ].
 Notation "'EX' x | p"      := (ex ? [x]p)
   (at level 10, p at level 8) : type_scope
-  V8only (at level 200, x ident, p at level 80).
+  V8only "'exists' x | p" (at level 200, x ident, p at level 80).
 Notation "'EX' x : t | p"  := (ex ? [x:t]p)
   (at level 10, p at level 8) : type_scope
-  V8only (at level 200, x ident, p at level 80).
+  V8only "'exists' x : t | p" (at level 200, x ident, p at level 80).
 
 V7only [ Notation Ex2 := (ex2 ?). ].
 Notation "'EX' x | p & q"       := (ex2 ? [x]p [x]q)
   (at level 10, p, q at level 8) : type_scope
-  V8only "'EX2' x | p & q" (at level 200, x ident, p, q at level 80).
+  V8only "'exists2' x | p & q" (at level 200, x ident, p, q at level 80).
 Notation "'EX' x : t | p & q"   := (ex2 ? [x:t]p [x:t]q)
   (at level 10, p, q at level 8) : type_scope
-  V8only "'EX2' x : t | p & q"
+  V8only "'exists2' x : t | p & q"
     (at level 200, x ident, t at level 200, p, q at level 80).
 
-V7only [Notation All := (all ?).].
+V7only [Notation All := (all ?).
 Notation "'ALL' x | p"     := (all ? [x]p)
   (at level 10, p at level 8) : type_scope
   V8only (at level 200, x ident, p at level 200).
 Notation "'ALL' x : t | p" := (all ? [x:t]p)
   (at level 10, p at level 8) : type_scope
   V8only (at level 200, x ident, t, p at level 200).
-
+].
 
 (** Universal quantification *)
 
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index ebf6a14d0..4f94658aa 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -525,7 +525,10 @@ let rec pr_vernac = function
   | VernacRestoreState s -> str"Restore State" ++ spc() ++ qsnew s
 
   (* Control *)
-  | VernacList l -> hov 2 (str"[" ++ spc() ++ prlist_with_sep (fun _ -> sep_end () ++ fnl() ) (pr_located pr_vernac) l ++ spc() ++ str"]") 
+  | VernacList l ->
+      hov 2 (str"[" ++ spc() ++
+             prlist (fun v -> pr_located pr_vernac v ++ sep_end () ++ fnl()) l
+             ++ spc() ++ str"]") 
   | VernacLoad (f,s) -> str"Load" ++ if f then (spc() ++ str"Verbose"
   ++ spc()) else spc()  ++ qsnew s
   | VernacTime v -> str"Time" ++ spc() ++ pr_vernac v