diff options
-rw-r--r-- | camlp4/etc/pr_o.ml | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/camlp4/etc/pr_o.ml b/camlp4/etc/pr_o.ml index c4f032069..e788f80cd 100644 --- a/camlp4/etc/pr_o.ml +++ b/camlp4/etc/pr_o.ml @@ -1496,14 +1496,6 @@ pr_patt.pr_levels := (S RO ",") al "" [: `S RO ")"; k :] :] :] | _ -> [: curr x "" [: :]; `next y "" k :] ] | p -> fun curr next dg k -> [: `next p "" k :] ]}; -(* - {pr_label = ""; pr_box _ x = HOVbox x; - pr_rules = - extfun Extfun.empty with - [ <:patt< $x$ . $y$ >> -> - fun curr next dg k -> [: curr x "" [: :]; `S NO "."; `next y "" k :] - | p -> fun curr next dg k -> [: `next p "" k :] ]}; -*) {pr_label = "simple"; pr_box p x = LocInfo (MLast.loc_of_patt p) (HOVbox x); pr_rules = |