diff options
| author | Emilio Jesus Gallego Arias | 2020-05-18 16:56:59 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-05-18 16:56:59 +0200 |
| commit | b456cf69eaac3e73f0c63c81ab2dbb58ca5e73b2 (patch) | |
| tree | a7c027e412d5aa616e3ec0a670390ff6b420bc31 /printing/printer.ml | |
| parent | b7c14a83d4a20dd9ba72c4ccc202ce0708dcd7e3 (diff) | |
| parent | 2d6dd66cf4e99e383da4af6a80f06b3d82395102 (diff) | |
Merge PR #11980: Improve spacing in Print Assumptions
Reviewed-by: ejgallego
Ack-by: herbelin
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 -> |