diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-19 17:04:07 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-19 17:49:50 +0100 |
| commit | f25396b3a35ea5cd64b8b68670e66a14a78c418c (patch) | |
| tree | 459c21960c2e43f85183fdd7fcd44f5e8bd1e93e /parsing/tok.ml | |
| parent | fff96bb174df956bc38c207d716d7f8019ca04d8 (diff) | |
Further reducing the dependencies of the EXTEND macros.
Diffstat (limited to 'parsing/tok.ml')
| -rw-r--r-- | parsing/tok.ml | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/parsing/tok.ml b/parsing/tok.ml index 6b9008615..df7e7c2a6 100644 --- a/parsing/tok.ml +++ b/parsing/tok.ml @@ -8,6 +8,8 @@ (** The type of token for the Coq lexer and parser *) +let string_equal (s1 : string) s2 = s1 = s2 + type t = | KEYWORD of string | PATTERNIDENT of string @@ -21,16 +23,16 @@ 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 -| PATTERNIDENT s1, PATTERNIDENT s2 -> CString.equal s1 s2 -| IDENT s1, IDENT s2 -> CString.equal s1 s2 -| FIELD s1, FIELD s2 -> CString.equal s1 s2 -| INT s1, INT s2 -> CString.equal s1 s2 -| INDEX s1, INDEX s2 -> CString.equal s1 s2 -| STRING s1, STRING s2 -> CString.equal s1 s2 +| IDENT s1, KEYWORD s2 -> string_equal s1 s2 +| KEYWORD s1, KEYWORD s2 -> string_equal s1 s2 +| PATTERNIDENT s1, PATTERNIDENT s2 -> string_equal s1 s2 +| IDENT s1, IDENT s2 -> string_equal s1 s2 +| FIELD s1, FIELD s2 -> string_equal s1 s2 +| INT s1, INT s2 -> string_equal s1 s2 +| INDEX s1, INDEX s2 -> string_equal s1 s2 +| STRING s1, STRING s2 -> string_equal s1 s2 | LEFTQMARK, LEFTQMARK -> true -| BULLET s1, BULLET s2 -> CString.equal s1 s2 +| BULLET s1, BULLET s2 -> string_equal s1 s2 | EOI, EOI -> true | _ -> false |