diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 5 | ||||
| -rw-r--r-- | printing/printer.ml | 7 |
2 files changed, 7 insertions, 5 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 2da163b8ee..b55a41471a 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -275,7 +275,7 @@ let tag_var = tag Tag.variable pr_reference r, latom | CPatOr pl -> - let pp = pr_patt mt (lpator,Any) in + let pp p = hov 0 (pr_patt mt (lpator,Any) p) in surround (hov 0 (prlist_with_sep pr_spcbar pp pl)), lpator | CPatNotation ((_,"( _ )"),([p],[]),[]) -> @@ -304,7 +304,8 @@ let tag_var = tag Tag.variable spc() ++ hov 4 (pr_with_comments ?loc (str "| " ++ - hov 0 (prlist_with_sep pr_spcbar (prlist_with_sep sep_v (pr_patt ltop)) pl + hov 0 (prlist_with_sep pr_spcbar + (fun p -> hov 0 (prlist_with_sep sep_v (pr_patt ltop) p)) pl ++ str " =>") ++ pr_sep_com spc (pr ltop) rhs)) diff --git a/printing/printer.ml b/printing/printer.ml index bb54f587fd..97e0528939 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -490,8 +490,8 @@ let pr_concl n ?(diffs=false) ?og_s sigma g = header ++ str " is:" ++ cut () ++ str" " ++ pc (* display evar type: a context and a type *) -let pr_evgl_sign sigma evi = - let env = evar_env evi in +let pr_evgl_sign env sigma evi = + let env = evar_env env evi in let ps = pr_named_context_of env sigma in let _, l = match Filter.repr (evar_filter evi) with | None -> [], [] @@ -517,7 +517,8 @@ let pr_evgl_sign sigma evi = (* Print an existential variable *) let pr_evar sigma (evk, evi) = - let pegl = pr_evgl_sign sigma evi in + let env = Global.env () in + let pegl = pr_evgl_sign env sigma evi in hov 0 (pr_existential_key sigma evk ++ str " : " ++ pegl) (* Print an enumerated list of existential variables *) |