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
---
 parsing/g_constrnew.ml4 | 16 +++++++++++-----
 parsing/g_tacticnew.ml4 | 38 ++++++++++++++++++++++++++++----------
 2 files changed, 39 insertions(+), 15 deletions(-)

(limited to 'parsing')

diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index ce45d73b08..9a9cf9a59e 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 b03aaf8680..fa9a402eb0 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 *)
-- 
cgit v1.2.3