diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-22 20:11:20 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-10-22 20:11:20 +0000 |
| commit | 5f8ce72b29f4a4620ce46895f2e563b2fd85f24b (patch) | |
| tree | 2886aafae6f2bca9436d2da714f6e6a9a275a1ba /parsing | |
| parent | 818ecca9f72b570ea2a3de47c783927616904b17 (diff) | |
Removing some generic equalities.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16915 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/tok.ml | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/parsing/tok.ml b/parsing/tok.ml index 4cb94e38b..0ff94d395 100644 --- a/parsing/tok.ml +++ b/parsing/tok.ml @@ -19,6 +19,18 @@ type t = | LEFTQMARK | EOI +let equal t1 t2 = match t1, t2 with +| KEYWORD s1, KEYWORD s2 -> CString.equal s1 s2 +| METAIDENT s1, METAIDENT 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 +| STRING s1, STRING s2 -> CString.equal s1 s2 +| LEFTQMARK, LEFTQMARK -> true +| EOI, EOI -> true +| _ -> false + let extract_string = function | KEYWORD s -> s | IDENT s -> s @@ -89,4 +101,4 @@ let match_pattern = | "EOI", "" -> (function EOI -> "" | _ -> err ()) | pat -> let tok = of_pattern pat in - function tok' -> if tok = tok' then snd pat else err () + function tok' -> if equal tok tok' then snd pat else err () |