diff options
| -rw-r--r-- | grammar/q_util.ml4 | 1 | ||||
| -rw-r--r-- | parsing/compat.ml4 | 1 | ||||
| -rw-r--r-- | parsing/g_constr.ml4 | 5 | ||||
| -rw-r--r-- | parsing/lexer.ml4 | 3 | ||||
| -rw-r--r-- | parsing/tok.ml | 7 | ||||
| -rw-r--r-- | parsing/tok.mli | 1 |
6 files changed, 1 insertions, 17 deletions
diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index d668e3d39..c6e2e9966 100644 --- a/grammar/q_util.ml4 +++ b/grammar/q_util.ml4 @@ -59,7 +59,6 @@ let mlexpr_of_ident id = let mlexpr_of_token = function | Tok.KEYWORD s -> <:expr< Tok.KEYWORD $mlexpr_of_string s$ >> -| Tok.METAIDENT s -> <:expr< Tok.METAIDENT $mlexpr_of_string s$ >> | Tok.PATTERNIDENT s -> <:expr< Tok.PATTERNIDENT $mlexpr_of_string s$ >> | Tok.IDENT s -> <:expr< Tok.IDENT $mlexpr_of_string s$ >> | Tok.FIELD s -> <:expr< Tok.FIELD $mlexpr_of_string s$ >> diff --git a/parsing/compat.ml4 b/parsing/compat.ml4 index 3405d2429..0e416fe32 100644 --- a/parsing/compat.ml4 +++ b/parsing/compat.ml4 @@ -262,7 +262,6 @@ IFDEF CAMLP5 THEN let pattern = match tok with | Tok.KEYWORD s -> "", s | Tok.IDENT s -> "IDENT", s - | Tok.METAIDENT s -> "METAIDENT", s | Tok.PATTERNIDENT s -> "PATTERNIDENT", s | Tok.FIELD s -> "FIELD", s | Tok.INT s -> "INT", s diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 1ac260ebe..0fe0ac42b 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -132,10 +132,7 @@ GEXTEND Gram closed_binder open_binders binder binders binders_fixannot record_declaration typeclass_constraint pattern appl_arg; Constr.ident: - [ [ id = Prim.ident -> id - - (* This is used in quotations and Syntax *) - | id = METAIDENT -> Id.of_string id ] ] + [ [ id = Prim.ident -> id ] ] ; Prim.name: [ [ "_" -> (!@loc, Anonymous) ] ] diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4 index 74e05ce84..232e9aee3 100644 --- a/parsing/lexer.ml4 +++ b/parsing/lexer.ml4 @@ -493,7 +493,6 @@ let process_chars bp c cs = err (bp, ep') Undefined_token let token_of_special c s = match c with - | '$' -> METAIDENT s | '.' -> FIELD s | _ -> assert false @@ -532,8 +531,6 @@ let blank_or_eof cs = let rec next_token = parser bp | [< '' ' | '\t' | '\n' |'\r' as c; s >] -> comm_loc bp; push_char c; next_token s - | [< ''$' as c; t = parse_after_special c bp >] ep -> - comment_stop bp; (t, (ep, bp)) | [< ''.' as c; t = parse_after_special c bp; s >] ep -> comment_stop bp; (* We enforce that "." should either be part of a larger keyword, diff --git a/parsing/tok.ml b/parsing/tok.ml index 4f50c48d0..6b9008615 100644 --- a/parsing/tok.ml +++ b/parsing/tok.ml @@ -10,7 +10,6 @@ type t = | KEYWORD of string - | METAIDENT of string | PATTERNIDENT of string | IDENT of string | FIELD of string @@ -24,7 +23,6 @@ type t = 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 | IDENT s1, IDENT s2 -> CString.equal s1 s2 | FIELD s1, FIELD s2 -> CString.equal s1 s2 @@ -40,7 +38,6 @@ let extract_string = function | KEYWORD s -> s | IDENT s -> s | STRING s -> s - | METAIDENT s -> s | PATTERNIDENT s -> s | FIELD s -> s | INT s -> s @@ -52,7 +49,6 @@ let extract_string = function let to_string = function | KEYWORD s -> Format.sprintf "%S" s | IDENT s -> Format.sprintf "IDENT %S" s - | METAIDENT s -> Format.sprintf "METAIDENT %S" s | PATTERNIDENT s -> Format.sprintf "PATTERNIDENT %S" s | FIELD s -> Format.sprintf "FIELD %S" s | INT s -> Format.sprintf "INT %s" s @@ -76,7 +72,6 @@ let print ppf tok = Format.pp_print_string ppf (to_string tok) let of_pattern = function | "", s -> KEYWORD s | "IDENT", s -> IDENT s - | "METAIDENT", s -> METAIDENT s | "PATTERNIDENT", s -> PATTERNIDENT s | "FIELD", s -> FIELD s | "INT", s -> INT s @@ -90,7 +85,6 @@ let of_pattern = function let to_pattern = function | KEYWORD s -> "", s | IDENT s -> "IDENT", s - | METAIDENT s -> "METAIDENT", s | PATTERNIDENT s -> "PATTERNIDENT", s | FIELD s -> "FIELD", s | INT s -> "INT", s @@ -105,7 +99,6 @@ let match_pattern = function | "", "" -> (function KEYWORD s -> s | _ -> err ()) | "IDENT", "" -> (function IDENT s -> s | _ -> err ()) - | "METAIDENT", "" -> (function METAIDENT s -> s | _ -> err ()) | "PATTERNIDENT", "" -> (function PATTERNIDENT s -> s | _ -> err ()) | "FIELD", "" -> (function FIELD s -> s | _ -> err ()) | "INT", "" -> (function INT s -> s | _ -> err ()) diff --git a/parsing/tok.mli b/parsing/tok.mli index f37de05a4..416ce468e 100644 --- a/parsing/tok.mli +++ b/parsing/tok.mli @@ -10,7 +10,6 @@ type t = | KEYWORD of string - | METAIDENT of string | PATTERNIDENT of string | IDENT of string | FIELD of string |