diff --git a/printing/printer.ml b/printing/printer.ml
index 31805556fc10e..1815b602cbbb6 100644
--- a/printing/printer.ml
+++ b/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 ->
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 42f795985c919..1e690c57a5570 100644
--- a/test-suite/output/Cases.out
+++ b/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
diff --git a/test-suite/output/DebugRelevances.out b/test-suite/output/DebugRelevances.out
index 468ffd26da70a..d94afb4602ea3 100644
--- a/test-suite/output/DebugRelevances.out
+++ b/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
diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
index b8db52735da5d..7dd5b298fe524 100644
--- a/test-suite/output/PrintAssumptions.out
+++ b/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: