diff options
| author | Gaëtan Gilbert | 2020-03-31 15:36:57 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-05-18 11:17:08 +0200 |
| commit | 2d6dd66cf4e99e383da4af6a80f06b3d82395102 (patch) | |
| tree | 977872d4e7058cfdd27e474634f6a7b6003496d6 /printing/printer.ml | |
| parent | b9591f15d75886456ff28984934de73d6a516af5 (diff) | |
Improve spacing in Print Assumptions
cf "If this is implemented, long names might cause a printing
problem:" in #11852
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index c2f73715f0..2ad9e268c2 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -905,7 +905,7 @@ let pr_assumptionset env sigma s = let pr_axiom env ax typ = match ax with | Constant kn -> - safe_pr_constant env kn ++ safe_pr_ltype env sigma typ + hov 1 (safe_pr_constant env kn ++ cut() ++ safe_pr_ltype env sigma typ) | Positive m -> hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is assumed to be positive.") | Guarded gr -> @@ -917,17 +917,17 @@ let pr_assumptionset env sigma s = let (v, a, o, tr) = accu in match t with | Variable id -> - let var = pr_id id ++ str " : " ++ pr_ltype_env env sigma typ in + let var = pr_id id ++ spc() ++ str ": " ++ pr_ltype_env env sigma typ in (var :: v, a, o, tr) | Axiom (axiom, []) -> let ax = pr_axiom env axiom typ in (v, ax :: a, o, tr) | Axiom (axiom,l) -> let ax = pr_axiom env axiom typ ++ - cut() ++ + spc() ++ prlist_with_sep cut (fun (lbl, ctx, ty) -> - str " used in " ++ Label.print lbl ++ - str " to prove:" ++ safe_pr_ltype_relctx (ctx,ty)) + str "used in " ++ Label.print lbl ++ + str " to prove" ++ fnl() ++ safe_pr_ltype_relctx (ctx,ty)) l in (v, ax :: a, o, tr) | Opaque kn -> |