Indent body and type when printing local definitions over several lines

printing/printer.ml

@@ -339,17 +339,19 @@ let get_compact_context,set_compact_context =
 let pr_compacted_decl env sigma decl =
   let ids, pbody, typ = match decl with
     | CompactedDecl.LocalAssum (ids, typ) ->
-       ids, mt (), typ
+       ids, None, typ
     | CompactedDecl.LocalDef (ids,c,typ) ->
        (* Force evaluation *)
        let pb = pr_lconstr_env ~inctx:true env sigma c in
        let pb = if isCast c then surround pb else pb in
-       ids, (str" := " ++ pb ++ cut ()), typ
-  in
-  let pids = prlist_with_sep pr_comma (fun id -> pr_id id.binder_name) ids in
+       ids, Some pb, typ in
+  let pids =
+    hov 0 (prlist_with_sep pr_comma (fun id -> pr_id id.binder_name) ids) in
   let pt = pr_ltype_env env sigma typ in
-  let ptyp = (str" : " ++ pt) in
-  hov 0 (pids ++ pbody ++ ptyp)
+  match pbody with
+  | None -> hov 2 (pids ++ str" :" ++ spc () ++ pt)
+  | Some pbody ->
+     hov 2 (pids ++ str" :=" ++ spc () ++ pbody ++ spc () ++ str": " ++ pt)
 
 let pr_ecompacted_decl env sigma (decl:EConstr.compacted_declaration) =
   let Refl = EConstr.Unsafe.eq in
@@ -374,8 +376,8 @@ let pr_rel_decl env sigma decl =
         (str":=" ++ spc () ++ pb ++ spc ()) in
   let ptyp = pr_ltype_env env sigma typ in
   match na with
-  | Anonymous -> hov 0 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
-  | Name id -> hov 0 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
+  | Anonymous -> hov 2 (str"<>" ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
+  | Name id -> hov 2 (pr_id id ++ spc () ++ pbody ++ str":" ++ spc () ++ ptyp)
 
 let pr_erel_decl env sigma (decl:EConstr.rel_declaration) =
   let Refl = EConstr.Unsafe.eq in
@@ -610,7 +612,7 @@ let pr_evgl_sign env sigma (evi : undefined evar_info) =
 let pr_evar sigma (evk, evi) =
   let env = Global.env () in
   let pegl = pr_evgl_sign env sigma evi in
-  hov 0 (pr_existential_key env sigma evk ++ str " : " ++ pegl)
+  hov 2 (pr_existential_key env sigma evk ++ str " :" ++ spc () ++ pegl)
 
 (* Print an enumerated list of existential variables *)
 let rec pr_evars_int_hd pr sigma i = function
@@ -1093,7 +1095,7 @@ let pr_assumptionset env sigma s =
         MutInd.print kn
     in
     let safe_pr_ltype env sigma typ =
-      try str " : " ++ pr_ltype_env env sigma typ
+      try str " :" ++ spc () ++ pr_ltype_env env sigma typ
       with e when CErrors.noncritical e -> mt ()
     in
     let safe_pr_ltype_relctx (rctx, typ) =
@@ -1104,7 +1106,7 @@ let pr_assumptionset env sigma s =
     let pr_axiom env ax typ =
       match ax with
       | Constant kn ->
-          hov 1 (safe_pr_constant env kn ++ cut() ++ safe_pr_ltype env sigma typ)
+          hov 2 (safe_pr_constant env kn ++ safe_pr_ltype env sigma typ)
       | Positive m ->
           hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is assumed to be positive.")
       | Guarded gr ->

test-suite/output/Cases.out

@@ -102,11 +102,11 @@ Arguments lem3 k
   n, n0 := match x + 0 with
            | 0 | S _ => 0
            end : nat
-  e,
-  e0 := match x + 0 as y return (y = y) with
-        | 0 => eq_refl
-        | S n => eq_refl
-        end : x + 0 = x + 0
+  e, e0 :=
+    match x + 0 as y return (y = y) with
+    | 0 => eq_refl
+    | S n => eq_refl
+    end : x + 0 = x + 0
   n1, n2 := match x with
             | 0 | S _ => 0
             end : nat
@@ -119,14 +119,14 @@ Arguments lem3 k
 1 goal
 
   p : nat
-  a,
-  a0 := match eq_refl as y in (_ = e) return (y = y /\ e = e) with
-        | eq_refl => conj eq_refl eq_refl
-        end : eq_refl = eq_refl /\ p = p
-  a1,
-  a2 := match eq_refl in (_ = e) return (p = p /\ e = e) with
-        | eq_refl => conj eq_refl eq_refl
-        end : p = p /\ p = p
+  a, a0 :=
+    match eq_refl as y in (_ = e) return (y = y /\ e = e) with
+    | eq_refl => conj eq_refl eq_refl
+    end : eq_refl = eq_refl /\ p = p
+  a1, a2 :=
+    match eq_refl in (_ = e) return (p = p /\ e = e) with
+    | eq_refl => conj eq_refl eq_refl
+    end : p = p /\ p = p
   ============================
   eq_refl = eq_refl
 fun x : comparison => match x with

test-suite/output/DebugRelevances.out

@@ -26,13 +26,13 @@ Arguments boz (A B)%type_scope a b
 1 goal
 
   f := fun (A : (* Relevant *) Type) (_ : (* α8 *) A) => A
-   : forall (A : (* Relevant *) Type) (_ : (* α8 *) A), Type
+    : forall (A : (* Relevant *) Type) (_ : (* α8 *) A), Type
   ============================
   True
 1 goal
 
   f := fun (A : (* Relevant *) Type) (_ : (* Relevant *) A) => A
-   : forall (A : (* Relevant *) Type) (_ : (* Relevant *) A), Type
+    : forall (A : (* Relevant *) Type) (_ : (* Relevant *) A), Type
   ============================
   True
 let x := 0 in x

test-suite/output/Naming.out

@@ -39,18 +39,20 @@
 1 goal
 
   x3, x, x1, x4, x0 : nat
-  H : forall x x3 : nat,
-      x + x1 = x4 + x3 ->
-      forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1)
+  H :
+    forall x x3 : nat,
+    x + x1 = x4 + x3 ->
+    forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (S x + x1)
   H0 : x + x1 = x4 + x0
   ============================
   forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x
 1 goal
 
   x3, x, x1, x4, x0 : nat
-  H : forall x x3 : nat,
-      x + x1 = x4 + x3 ->
-      forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (Datatypes.S x + x1)
+  H :
+    forall x x3 : nat,
+    x + x1 = x4 + x3 ->
+    forall x0 x4 x5 S0 : nat, x0 + S0 = x4 + x5 + (Datatypes.S x + x1)
   H0 : x + x1 = x4 + x0
   x5, x6, x7, S : nat
   ============================

test-suite/output/Notations.out

@@ -135,8 +135,9 @@ match x with
 end
      : list ?T -> option (list ?T)
 where
-?T : [x : list ?T  x1 : list ?T  x0 := x1 : list ?T |- Type] (x, x1,
-     x0 cannot be used)
+?T :
+  [x : list ?T  x1 : list ?T  x0 := x1 : list ?T |- Type] (x, x1,
+  x0 cannot be used)
 s
      : s
 10

test-suite/output/Notations4.out

@@ -44,22 +44,28 @@ fun y : nat => # (x, z) |-> y & y
      : forall y : nat,
        (?T1 * ?T2 -> ?T1 * ?T2 * nat) * (?T * ?T0 -> ?T * ?T0 * nat)
 where
-?T : [y : nat  pat : ?T * ?T0  p0 : ?T * ?T0  p := p0 : ?T * ?T0
-     |- Type] (pat, p0, p cannot be used)
-?T0 : [y : nat  pat : ?T * ?T0  p0 : ?T * ?T0  p := p0 : ?T * ?T0
-      |- Type] (pat, p0, p cannot be used)
-?T1 : [y : nat  pat : ?T1 * ?T2  p0 : ?T1 * ?T2  p := p0 : ?T1 * ?T2
-      |- Type] (pat, p0, p cannot be used)
-?T2 : [y : nat  pat : ?T1 * ?T2  p0 : ?T1 * ?T2  p := p0 : ?T1 * ?T2
-      |- Type] (pat, p0, p cannot be used)
+?T :
+  [y : nat  pat : ?T * ?T0  p0 : ?T * ?T0  p := p0 : ?T * ?T0 |- Type] (pat,
+  p0, p cannot be used)
+?T0 :
+  [y : nat  pat : ?T * ?T0  p0 : ?T * ?T0  p := p0 : ?T * ?T0 |- Type] (pat,
+  p0, p cannot be used)
+?T1 :
+  [y : nat  pat : ?T1 * ?T2  p0 : ?T1 * ?T2  p := p0 : ?T1 * ?T2
+  |- Type] (pat, p0, p cannot be used)
+?T2 :
+  [y : nat  pat : ?T1 * ?T2  p0 : ?T1 * ?T2  p := p0 : ?T1 * ?T2
+  |- Type] (pat, p0, p cannot be used)
 fun y : nat => # (x, z) |-> (x + y) & (y + z)
      : forall y : nat,
        (nat * ?T -> nat * ?T * nat) * (?T0 * nat -> ?T0 * nat * nat)
 where
-?T : [y : nat  pat : nat * ?T  p0 : nat * ?T  p := p0 : nat * ?T
-     |- Type] (pat, p0, p cannot be used)
-?T0 : [y : nat  pat : ?T0 * nat  p0 : ?T0 * nat  p := p0 : ?T0 * nat
-      |- Type] (pat, p0, p cannot be used)
+?T :
+  [y : nat  pat : nat * ?T  p0 : nat * ?T  p := p0 : nat * ?T |- Type] (pat,
+  p0, p cannot be used)
+?T0 :
+  [y : nat  pat : ?T0 * nat  p0 : ?T0 * nat  p := p0 : ?T0 * nat
+  |- Type] (pat, p0, p cannot be used)
 fun '{| |} => true
      : R -> bool
 File "./output/Notations4.v", line 149, characters 82-85:

test-suite/output/PrintAssumptions.out

@@ -9,17 +9,17 @@ bli : Type
 Axioms:
 seq relies on definitional UIP.
 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: