diff options
| author | Tej Chajed | 2020-02-24 13:31:55 -0500 |
|---|---|---|
| committer | Tej Chajed | 2020-02-24 13:31:55 -0500 |
| commit | da984ceafbb450dc5a9fe8f8971d8c90a060f233 (patch) | |
| tree | d852c4393dc5630e7e667f5b37a481343d23fa3b | |
| parent | 46fe9b26ad55a266b71bbd428ee406b03a9db030 (diff) | |
| parent | 059da3541f54311283067cb3010b539506cb70bd (diff) | |
Merge PR #11560: Fix #11549: Ltac2 is incompatible with $.
Reviewed-by: tchajed
| -rw-r--r-- | test-suite/bugs/closed/bug_11549.v | 5 | ||||
| -rw-r--r-- | user-contrib/Ltac2/g_ltac2.mlg | 12 |
2 files changed, 11 insertions, 6 deletions
diff --git a/test-suite/bugs/closed/bug_11549.v b/test-suite/bugs/closed/bug_11549.v new file mode 100644 index 0000000000..7608e1c4d8 --- /dev/null +++ b/test-suite/bugs/closed/bug_11549.v @@ -0,0 +1,5 @@ +From Ltac2 Require Ltac2. + +Notation "t $ r" := (t r) + (at level 65, right associativity, only parsing). +Check S $ O. diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index d05640f22d..1c66fee9b8 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -25,6 +25,10 @@ let err () = raise Stream.Failure type lookahead = Gramlib.Plexing.location_function -> int -> Tok.t Stream.t -> int option +let check_no_space tok m strm = + let n = Stream.count strm in + if G_prim.contiguous tok n (n+m-1) then Some m else None + let entry_of_lookahead s (lk : lookahead) = let run tok strm = match lk tok 0 strm with None -> err () | Some _ -> () in Pcoq.Entry.of_parser s run @@ -51,7 +55,7 @@ let lk_int tok n strm = match stream_nth n strm with | NUMERAL { NumTok.int = _; frac = ""; exp = "" } -> Some (n + 1) | _ -> None -let lk_ident_or_anti = lk_ident <+> (lk_kw "$" >> lk_ident) +let lk_ident_or_anti = lk_ident <+> (lk_kw "$" >> lk_ident >> check_no_space) let rec lk_ident_list n strm = ((lk_ident >> lk_ident_list) <+> lk_empty) n strm @@ -80,10 +84,6 @@ let test_lpar_id_rpar = lk_kw "(" >> lk_ident >> lk_kw ")" end -let check_no_space tok m strm = - let n = Stream.count strm in - if G_prim.contiguous tok n (n+m-1) then Some m else None - let test_ampersand_ident = entry_of_lookahead "test_ampersand_ident" begin lk_kw "&" >> lk_ident >> check_no_space @@ -91,7 +91,7 @@ let test_ampersand_ident = let test_dollar_ident = entry_of_lookahead "test_dollar_ident" begin - lk_kw "$" >> lk_ident + lk_kw "$" >> lk_ident >> check_no_space end let test_ltac1_env = |