diff options
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 *) |