diff options
Diffstat (limited to 'coqpp')
| -rw-r--r-- | coqpp/coqpp_main.ml | 15 |
1 files changed, 3 insertions, 12 deletions
diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 90158c3aa3..c8a87e6cb6 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -212,17 +212,9 @@ let print_fun fmt (vars, body) = (** Meta-program instead of calling Tok.of_pattern here because otherwise violates value restriction *) -let print_tok fmt = function -| "", s -> fprintf fmt "Tok.KEYWORD %a" print_string s -| "IDENT", s -> fprintf fmt "Tok.IDENT %a" print_string s -| "PATTERNIDENT", s -> fprintf fmt "Tok.PATTERNIDENT %a" print_string s -| "FIELD", s -> fprintf fmt "Tok.FIELD %a" print_string s -| "INT", s -> fprintf fmt "Tok.INT %a" print_string s -| "STRING", s -> fprintf fmt "Tok.STRING %a" print_string s -| "LEFTQMARK", _ -> fprintf fmt "Tok.LEFTQMARK" -| "BULLET", s -> fprintf fmt "Tok.BULLET %a" print_string s -| "EOI", _ -> fprintf fmt "Tok.EOI" -| _ -> failwith "Tok.of_pattern: not a constructor" +let print_tok fmt (k,o) = + let print_pat fmt = print_opt fmt print_string in + fprintf fmt "(%a,%a)" print_string k print_pat o let rec print_prod fmt p = let (vars, tkns) = List.split p.gprod_symbs in @@ -240,7 +232,6 @@ and print_symbols fmt = function and print_symbol fmt tkn = match tkn with | SymbToken (t, s) -> - let s = match s with None -> "" | Some s -> s in fprintf fmt "(Extend.Atoken (%a))" print_tok (t, s) | SymbEntry (e, None) -> fprintf fmt "(Extend.Aentry %s)" e |