diff options
| -rw-r--r-- | printing/printer.ml | 10 | ||||
| -rw-r--r-- | test-suite/output/PrintAssumptions.out | 16 |
2 files changed, 13 insertions, 13 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 -> diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out index 190c34262f..ca4858d7a7 100644 --- a/test-suite/output/PrintAssumptions.out +++ b/test-suite/output/PrintAssumptions.out @@ -7,17 +7,17 @@ bli : Type Axioms: bli : Type Axioms: -extensionality : forall (P Q : Type) (f g : P -> Q), - (forall x : P, f x = g x) -> f = g +extensionality + : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g Axioms: -extensionality : forall (P Q : Type) (f g : P -> Q), - (forall x : P, f x = g x) -> f = g +extensionality + : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g Axioms: -extensionality : forall (P Q : Type) (f g : P -> Q), - (forall x : P, f x = g x) -> f = g +extensionality + : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g Axioms: -extensionality : forall (P Q : Type) (f g : P -> Q), - (forall x : P, f x = g x) -> f = g +extensionality + : forall (P Q : Type) (f g : P -> Q), (forall x : P, f x = g x) -> f = g Closed under the global context Closed under the global context Axioms: |