diff options
| author | barras | 2003-10-11 00:20:33 +0000 |
|---|---|---|
| committer | barras | 2003-10-11 00:20:33 +0000 |
| commit | 2b61cb974c847669eaf24dfbf47d8615812481fb (patch) | |
| tree | 114bfc378dbb08e18ab57c4072277b4dc0a5fd04 /parsing | |
| parent | e5164cf5448cb25d2911320469bc16e44ceae511 (diff) | |
mise a jour nouvelle syntaxe
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4595 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_constrnew.ml4 | 16 | ||||
| -rw-r--r-- | parsing/g_tacticnew.ml4 | 38 |
2 files changed, 39 insertions, 15 deletions
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 *) |