diff options
Diffstat (limited to 'printing/ppconstr.ml')
| -rw-r--r-- | printing/ppconstr.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 9d3ed40f6c..8d5213b988 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -249,7 +249,7 @@ let tag_var = tag Tag.variable str"@{" ++ hov 0 (prlist_with_sep pr_semicolon f (List.rev l)) ++ str"}")) let las = lapp - let lpator = 100 + let lpator = 0 let lpatrec = 0 let rec pr_patt sep inh p = @@ -283,7 +283,8 @@ let tag_var = tag Tag.variable pr_reference r, latom | CPatOr pl -> - hov 0 (prlist_with_sep pr_spcbar (pr_patt mt (lpator,L)) pl), lpator + let pp = pr_patt mt (lpator,Any) in + surround (hov 0 (prlist_with_sep pr_spcbar pp pl)), lpator | CPatNotation ((_,"( _ )"),([p],[]),[]) -> pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom @@ -348,7 +349,7 @@ let tag_var = tag Tag.variable hov 1 (str "`" ++ (surround_impl b' (pr_lident CAst.(make ?loc id) ++ str " : " ++ (if t' then str "!" else mt()) ++ pr t))) - |_ -> anomaly (Pp.str "List of generalized binders have alwais one element.") + |_ -> anomaly (Pp.str "List of generalized binders have always one element.") end | Default b -> match t with |