Indent body and type when printing local definitions over several lines.

For instance:

Theorem T (long_long_long_long_long_long_long_long_ident := fun x : nat => x) : True.

Before:

  long_long_long_long_long_long_long_long_ident :=
  fun x : nat => x : nat -> nat
  ============================
  True

After:

  long_long_long_long_long_long_long_long_ident :=
    fun x : nat => x : nat -> nat
  ============================
  True

At the same time, we:
- improve the printing of multiple variables with same time (see test-suite)
- adopt the conventional +2 indentation in Print Assumptions in place of
  an exceptional +1 indentation for axioms

printing/printer.ml

@@ -346,10 +346,10 @@ let pr_compacted_decl env sigma decl =
        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
+  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)
+  hov 2 (pids ++ pbody ++ ptyp)
 
 let pr_ecompacted_decl env sigma (decl:EConstr.compacted_declaration) =
   let Refl = EConstr.Unsafe.eq in
@@ -374,8 +374,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 +610,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 " : " ++ pegl)
 
 (* Print an enumerated list of existential variables *)
 let rec pr_evars_int_hd pr sigma i = function
@@ -1104,7 +1104,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 ++ 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 ->

test-suite/output/Cases.out

@@ -102,11 +102,10 @@ 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 +118,12 @@ 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/PrintAssumptions.out

@@ -10,16 +10,16 @@ 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
+   : 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
+   : 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
+   : 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
+   : 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: