aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/ppconstr.ml
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-01-17 23:40:35 +0100
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-04-25 00:00:43 +0200
commit30d3515546cf244837c6340b6b87c5f51e68cbf4 (patch)
tree70dd074f483c34e9f71da20edf878062a4b5b3af /printing/ppconstr.ml
parent84eb5cd72a015c45337a5a6070c5651f56be6e74 (diff)
[location] Remove Loc.ghost.
Now it is a private field, locations are optional.
Diffstat (limited to 'printing/ppconstr.ml')
-rw-r--r--printing/ppconstr.ml10
1 files changed, 5 insertions, 5 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 117e1900d..fddd54a9f 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -145,9 +145,9 @@ let tag_var = tag Tag.variable
if !Flags.beautify && not (Int.equal n 0) then comment (CLexer.extract_comments n)
else mt()
- let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
+ let pr_with_comments ?loc pp = pr_located (fun x -> x) (Loc.tag ?loc pp)
- let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c)
+ let pr_sep_com sep f c = pr_with_comments ~loc:(constr_loc c) (sep() ++ f c)
let pr_univ l =
match l with
@@ -302,7 +302,7 @@ let tag_var = tag Tag.variable
assert false
in
let loc = cases_pattern_expr_loc (loc, p) in
- pr_with_comments loc
+ pr_with_comments ~loc
(sep() ++ if prec_less prec inh then strm else surround strm)
let pr_patt = pr_patt mt
@@ -310,7 +310,7 @@ let tag_var = tag Tag.variable
let pr_eqn pr (loc,(pl,rhs)) =
let pl = List.map snd pl in
spc() ++ hov 4
- (pr_with_comments loc
+ (pr_with_comments ~loc
(str "| " ++
hov 0 (prlist_with_sep pr_bar (prlist_with_sep sep_v (pr_patt ltop)) pl
++ str " =>") ++
@@ -730,7 +730,7 @@ let tag_var = tag Tag.variable
return (pr_delimiters sc (pr mt (ldelim,E) a), ldelim)
in
let loc = constr_loc a in
- pr_with_comments loc
+ pr_with_comments ~loc
(sep() ++ if prec_less prec inherited then strm else surround strm)
type term_pr = {