diff options
| author | Enrico Tassi | 2019-08-02 16:50:22 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2019-08-06 16:02:01 +0200 |
| commit | 97d739835e98dcca038970a50e169a4e1127bd80 (patch) | |
| tree | 3b1628d0a48e51c25772ef9ae9b97731a1a1ddc2 /user-contrib | |
| parent | cb1557bd32ad84b0af278ed040aa207547e0df5d (diff) | |
[parsing] unify checks for contiguity of tokens in Ltac2 and G_prim
Diffstat (limited to 'user-contrib')
| -rw-r--r-- | user-contrib/Ltac2/g_ltac2.mlg | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg index 8e5aae4900..adc1606016 100644 --- a/user-contrib/Ltac2/g_ltac2.mlg +++ b/user-contrib/Ltac2/g_ltac2.mlg @@ -82,9 +82,7 @@ let test_lpar_id_rpar = let check_no_space tok m strm = let n = Stream.count strm in - let (_, ep) = Loc.unloc (tok n) in - let (bp, _) = Loc.unloc (tok (n + 1)) in - if Int.equal ep bp then Some m else None + 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 |