diff options
| author | Pierre-Marie Pédrot | 2015-11-29 19:05:53 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-11-29 19:13:30 +0100 |
| commit | e98d3c3793f26265a49f63a6e78d704f88341df9 (patch) | |
| tree | c0328afc0034f3262dca2ca067531ee19bbb0ee0 /parsing | |
| parent | 103ec7205d9038f1f3821f9287e3bb0907a1e3ec (diff) | |
| parent | 8d6e58e16cc53a3198eb4c4afef0a2c39f6a5c56 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/tok.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/tok.ml b/parsing/tok.ml index efd57968d2..12140f4036 100644 --- a/parsing/tok.ml +++ b/parsing/tok.ml @@ -21,6 +21,7 @@ type t = | EOI let equal t1 t2 = match t1, t2 with +| IDENT s1, KEYWORD s2 -> CString.equal s1 s2 | KEYWORD s1, KEYWORD s2 -> CString.equal s1 s2 | METAIDENT s1, METAIDENT s2 -> CString.equal s1 s2 | PATTERNIDENT s1, PATTERNIDENT s2 -> CString.equal s1 s2 |