diff options
Diffstat (limited to 'parsing/g_rsyntax.ml')
| -rw-r--r-- | parsing/g_rsyntax.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_rsyntax.ml b/parsing/g_rsyntax.ml index ff42bc01d..41fe0df2a 100644 --- a/parsing/g_rsyntax.ml +++ b/parsing/g_rsyntax.ml @@ -71,13 +71,13 @@ let replace_plus p = let r_printer std_pr p = let (_,ast1,astp,_) = get_r_sign dummy_loc in match (int_of_r p) with - | Some i -> [< 'sTR (string_of_int (i+1)) >] + | Some i -> (str (string_of_int (i+1))) | None -> std_pr (replace_plus p) let r_printer_outside std_pr p = let (_,ast1,astp,_) = get_r_sign dummy_loc in match (int_of_r p) with - | Some i -> [< 'sTR "``"; 'sTR (string_of_int (i+1)); 'sTR "``" >] + | Some i -> (str "``" ++ str (string_of_int (i+1)) ++ str "``") | None -> std_pr (replace_plus p) let _ = Esyntax.Ppprim.add ("r_printer", r_printer) |