aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/ppconstr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/ppconstr.ml')
-rw-r--r--parsing/ppconstr.ml14
1 files changed, 10 insertions, 4 deletions
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index 0f0c38adc..04b700236 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -674,10 +674,16 @@ let pr_cases_pattern_expr = pr_patt ltop
let pr_binders = pr_undelimited_binders (pr ltop)
-let pr_with_occurrences pr = function
- ([],c) -> pr c
- | (nl,c) -> hov 1 (pr c ++ spc() ++ str"at " ++
- hov 0 (prlist_with_sep spc (pr_or_var int) nl))
+let pr_with_occurrences_with_trailer pr occs trailer =
+ match occs with
+ ((false,[]),c) -> pr c ++ trailer
+ | ((nowhere_except_in,nl),c) ->
+ hov 1 (pr c ++ spc() ++ str"at " ++
+ (if nowhere_except_in then mt() else str "- ") ++
+ hov 0 (prlist_with_sep spc (pr_or_var int) nl) ++ trailer)
+
+let pr_with_occurrences pr occs =
+ pr_with_occurrences_with_trailer pr occs (mt())
let pr_red_flag pr r =
(if r.rBeta then pr_arg str "beta" else mt ()) ++