diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean
index a895c7dc04..ab2d244e3b 100644
--- a/src/Lean/Elab/Print.lean
+++ b/src/Lean/Elab/Print.lean
@@ -22,7 +22,7 @@ private def levelParamsToMessageData (levelParams : List Name) : MessageData :=
       m := m ++ ", " ++ toMessageData u
     return m ++ "}"
 
-private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (safety : DefinitionSafety) : CommandElabM MessageData := do
+private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (safety : DefinitionSafety) (sig : Bool := true) : CommandElabM MessageData := do
   let m : MessageData :=
     match (← getReducibilityStatus id) with
     | ReducibilityStatus.irreducible => "@[irreducible] "
@@ -38,11 +38,13 @@ private def mkHeader (kind : String) (id : Name) (levelParams : List Name) (type
   let (m, id) := match privateToUserName? id with
     | some id => (m ++ "private ", id)
     | none    => (m, id)
-  let m := m ++ kind ++ " " ++ id ++ levelParamsToMessageData levelParams ++ " : " ++ type
-  pure m
+  if sig then
+    return m!"{m}{kind} {id}{levelParamsToMessageData levelParams} : {type}"
+  else
+    return m!"{m}{kind}"
 
-private def mkHeader' (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (isUnsafe : Bool) : CommandElabM MessageData :=
-  mkHeader kind id levelParams type (if isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe)
+private def mkHeader' (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (isUnsafe : Bool) (sig : Bool := true) : CommandElabM MessageData :=
+  mkHeader kind id levelParams type (if isUnsafe then DefinitionSafety.unsafe else DefinitionSafety.safe) (sig := sig)
 
 private def printDefLike (kind : String) (id : Name) (levelParams : List Name) (type : Expr) (value : Expr) (safety := DefinitionSafety.safe) : CommandElabM Unit := do
   let m ← mkHeader kind id levelParams type safety
@@ -65,32 +67,63 @@ private def printInduct (id : Name) (levelParams : List Name) (numParams : Nat)
     m := m ++ Format.line ++ ctor ++ " : " ++ cinfo.type
   logInfo m
 
+/--
+Computes the origin of a field. Returns its projection function at the origin.
+Multiple parents could be the origin of a field, but we say the first parent that provides it is the one that determines the origin.
+-/
+private partial def getFieldOrigin (structName field : Name) : MetaM Name := do
+  let env ← getEnv
+  for parent in getStructureParentInfo env structName do
+    if (findField? env parent.structName field).isSome then
+      return ← getFieldOrigin parent.structName field
+  let some fi := getFieldInfo? env structName field
+    | throwError "no such field {field} in {structName}"
+  return fi.projFn
+
 open Meta in
 private def printStructure (id : Name) (levelParams : List Name) (numParams : Nat) (type : Expr)
-    (ctor : Name) (fields : Array Name) (isUnsafe : Bool) (isClass : Bool) : CommandElabM Unit := do
-  let kind := if isClass then "class" else "structure"
-  let mut m ← mkHeader' kind id levelParams type isUnsafe
-  m := m ++ Format.line ++ "number of parameters: " ++ toString numParams
-  m := m ++ Format.line ++ "constructor:"
-  let cinfo ← getConstInfo ctor
-  m := m ++ Format.line ++ ctor ++ " : " ++ cinfo.type
-  m := m ++ Format.line ++ "fields:" ++ (← doFields)
-  logInfo m
-where
-  doFields := liftTermElabM do
-    forallTelescope (← getConstInfo id).type fun params _ =>
-      withLocalDeclD `self (mkAppN (Expr.const id (levelParams.map .param)) params) fun self => do
-        let params := params.push self
-        let mut m : MessageData := ""
+    (isUnsafe : Bool) : CommandElabM Unit := do
+  let env ← getEnv
+  let kind := if isClass env id then "class" else "structure"
+  let header ← mkHeader' kind id levelParams type isUnsafe (sig := false)
+  liftTermElabM <| forallTelescope (← getConstInfo id).type fun params _ =>
+    let s := Expr.const id (levelParams.map .param)
+    withLocalDeclD `self (mkAppN s params) fun self => do
+      let mut m : MessageData := header
+      -- Signature
+      m := m ++ " " ++ .ofFormatWithInfosM do
+        let (stx, infos) ← PrettyPrinter.delabCore s (delab := PrettyPrinter.Delaborator.delabConstWithSignature)
+        pure ⟨← PrettyPrinter.ppTerm ⟨stx⟩, infos⟩
+      m := m ++ Format.line ++ m!"number of parameters: {numParams}"
+      -- Parents
+      let parents := getStructureParentInfo env id
+      unless parents.isEmpty do
+        m := m ++ Format.line ++ "parents:"
+        for parent in parents do
+          let ptype ← inferType (mkApp (mkAppN (.const parent.projFn (levelParams.map .param)) params) self)
+          m := m ++ indentD m!"{.ofConstName parent.projFn (fullNames := true)} : {ptype}"
+      -- Fields
+      let fields := getStructureFieldsFlattened env id (includeSubobjectFields := false)
+      if fields.isEmpty then
+        m := m ++ Format.line ++ "fields: (none)"
+      else
+        m := m ++ Format.line ++ "fields:"
         for field in fields do
-          match getProjFnForField? (← getEnv) id field with
-          | some proj =>
-            let field : Format := if isPrivateName proj then "private " ++ toString field else toString field
-            let cinfo ← getConstInfo proj
-            let ftype ← instantiateForall cinfo.type params
-            m := m ++ Format.line ++ field ++ " : " ++ ftype
-          | none => panic! "missing structure field info"
-        addMessageContext m
+          let some source := findField? env id field | panic! "missing structure field info"
+          let proj ← getFieldOrigin source field
+          let modifier := if isPrivateName proj then "private " else ""
+          let ftype ← inferType (← mkProjection self field)
+          m := m ++ indentD (m!"{modifier}{.ofConstName proj (fullNames := true)} : {ftype}")
+      -- Constructor
+      let cinfo := getStructureCtor (← getEnv) id
+      let ctorModifier := if isPrivateName cinfo.name then "private " else ""
+      m := m ++ Format.line ++ "constructor:" ++ indentD (ctorModifier ++ .signature cinfo.name)
+      -- Resolution order
+      let resOrder ← getStructureResolutionOrder id
+      if resOrder.size > 1 then
+        m := m ++ Format.line ++ "resolution order:"
+          ++ indentD (MessageData.joinSep (resOrder.map (.ofConstName · (fullNames := true))).toList ", ")
+      logInfo m
 
 private def printIdCore (id : Name) : CommandElabM Unit := do
   let env ← getEnv
@@ -103,11 +136,10 @@ private def printIdCore (id : Name) : CommandElabM Unit := do
   | ConstantInfo.ctorInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "constructor" id us t u
   | ConstantInfo.recInfo { levelParams := us, type := t, isUnsafe := u, .. } => printAxiomLike "recursor" id us t u
   | ConstantInfo.inductInfo { levelParams := us, numParams, type := t, ctors, isUnsafe := u, .. } =>
-    match getStructureInfo? env id with
-    | some { fieldNames, .. } =>
-      let [ctor] := ctors | panic! "structures have only one constructor"
-      printStructure id us numParams t ctor fieldNames u (isClass env id)
-    | none => printInduct id us numParams t ctors u
+    if isStructure env id then
+      printStructure id us numParams t u
+    else
+      printInduct id us numParams t ctors u
   | none => throwUnknownId id
 
 private def printId (id : Syntax) : CommandElabM Unit := do
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 8d106035e4..22a6bf99f0 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -91,21 +91,32 @@ Rather, it is called through the `app` delaborator.
 -/
 def delabConst : Delab := do
   let Expr.const c₀ ls ← getExpr | unreachable!
-  let c₀ := if (← getPPOption getPPPrivateNames) then c₀ else (privateToUserName? c₀).getD c₀
-
-  let mut c ← unresolveNameGlobal c₀ (fullNames := ← getPPOption getPPFullNames)
-  let stx ← if ls.isEmpty || !(← getPPOption getPPUniverses) then
-    if (← getLCtx).usesUserName c then
-      -- `c` is also a local declaration
-      if c == c₀ && !(← read).inPattern then
-        -- `c` is the fully qualified named. So, we append the `_root_` prefix
-        c := `_root_ ++ c
+  let mut c₀ := c₀
+  let mut c  := c₀
+  if let some n := privateToUserName? c₀ then
+    unless (← getPPOption getPPPrivateNames) do
+      if c₀ == mkPrivateName (← getEnv) n then
+        -- The name is defined in this module, so use `n` as the name and unresolve like any other name.
+        c₀ := n
+        c ← unresolveNameGlobal n (fullNames := ← getPPOption getPPFullNames)
       else
-        c := c₀
-    pure <| mkIdent c
+        -- The name is not defined in this module, so make inaccessible. Unresolving does not make sense to do.
+        c ← withFreshMacroScope <| MonadQuotation.addMacroScope n
   else
-    let mvars ← getPPOption getPPMVarsLevels
-    `($(mkIdent c).{$[$(ls.toArray.map (Level.quote · (prec := 0) (mvars := mvars)))],*})
+    c ← unresolveNameGlobal c (fullNames := ← getPPOption getPPFullNames)
+  let stx ←
+    if ls.isEmpty || !(← getPPOption getPPUniverses) then
+      if (← getLCtx).usesUserName c then
+        -- `c` is also a local declaration
+        if c == c₀ && !(← read).inPattern then
+          -- `c` is the fully qualified named. So, we append the `_root_` prefix
+          c := `_root_ ++ c
+        else
+          c := c₀
+      pure <| mkIdent c
+    else
+      let mvars ← getPPOption getPPMVarsLevels
+      `($(mkIdent c).{$[$(ls.toArray.map (Level.quote · (prec := 0) (mvars := mvars)))],*})
 
   let stx ← maybeAddBlockImplicit stx
   if (← getPPOption getPPTagAppFns) then
diff --git a/tests/lean/diamond1.lean.expected.out b/tests/lean/diamond1.lean.expected.out
index 49118dbdb3..a7c8f62c67 100644
--- a/tests/lean/diamond1.lean.expected.out
+++ b/tests/lean/diamond1.lean.expected.out
@@ -2,14 +2,20 @@ diamond1.lean:11:40-11:45: error: parent field type mismatch, field 'a' from par
   α → α : Type
 but is expected to have type
   α : Type
-structure Foo : Type → Type
+structure Foo (α : Type) : Type
 number of parameters: 1
-constructor:
-Foo.mk : {α : Type} → Bar (α → α) → (Bool → α) → Nat → Foo α
+parents:
+  Foo.toBar : Bar (α → α)
+  Foo.toBaz : Baz α
 fields:
-toBar : Bar (α → α)
-c : Bool → α
-d : Nat
+  Bar.a : α → α
+  Bar.b : Nat → α → α
+  Baz.c : Bool → α
+  Baz.d : Nat
+constructor:
+  Foo.mk {α : Type} (toBar : Bar (α → α)) (c : Bool → α) (d : Nat) : Foo α
+resolution order:
+  Foo, Bar, Baz
 def f : Nat → Foo Nat :=
 fun x => { a := fun y => x + y, b := fun x1 x2 => x1 + x2, c := fun x_1 => x, d := x }
 diamond1.lean:27:47-27:52: warning: field 'a' from 'Baz' has already been declared
diff --git a/tests/lean/diamond8.lean.expected.out b/tests/lean/diamond8.lean.expected.out
index 6dbbcd8b7b..07f82208a1 100644
--- a/tests/lean/diamond8.lean.expected.out
+++ b/tests/lean/diamond8.lean.expected.out
@@ -1,7 +1,16 @@
-class Semiring.{u} : Type u → Type u
+class Semiring.{u} (R : Type u) : Type u
 number of parameters: 1
-constructor:
-Semiring.mk : {R : Type u} → [toAddCommMonoid : AddCommMonoid R] → [toMonoid : Monoid R] → Semiring R
+parents:
+  Semiring.toAddCommMonoid : AddCommMonoid R
+  Semiring.toMonoidWithZero : MonoidWithZero R
+  Semiring.toOne : One R
 fields:
-toAddCommMonoid : AddCommMonoid R
-toMonoid : Monoid R
+  Add.add : R → R → R
+  Zero.zero : R
+  Mul.mul : R → R → R
+  One.one : R
+  Monoid.mul_one : ∀ (m : R), m * 1 = m
+constructor:
+  Semiring.mk.{u} {R : Type u} [toAddCommMonoid : AddCommMonoid R] [toMonoid : Monoid R] : Semiring R
+resolution order:
+  Semiring, AddCommMonoid, MonoidWithZero, Add, Monoid, Zero, Mul, One
diff --git a/tests/lean/printStructure.lean b/tests/lean/printStructure.lean
index 7c3685f6f6..b867ef066d 100644
--- a/tests/lean/printStructure.lean
+++ b/tests/lean/printStructure.lean
@@ -1,94 +1,152 @@
 /-!
-  Test #print command for structures and classes
+# Test `#print` command for structures and classes
 -/
 
-/- Structure -/
+/-! Structure -/
 /--
-info: structure Prod.{u, v} : Type u → Type v → Type (max u v)
+info: structure Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)
 number of parameters: 2
-constructor:
-Prod.mk : {α : Type u} → {β : Type v} → α → β → α × β
 fields:
-fst : α
-snd : β
+  Prod.fst : α
+  Prod.snd : β
+constructor:
+  Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × β
 -/
 #guard_msgs in
 #print Prod
 
-/- Class -/
+/-! Class -/
 /--
-info: class Inhabited.{u} : Sort u → Sort (max 1 u)
+info: class Inhabited.{u} (α : Sort u) : Sort (max 1 u)
 number of parameters: 1
-constructor:
-Inhabited.mk : {α : Sort u} → α → Inhabited α
 fields:
-default : α
+  Inhabited.default : α
+constructor:
+  Inhabited.mk.{u} {α : Sort u} (default : α) : Inhabited α
 -/
 #guard_msgs in
 #print Inhabited
 
-/- Structure with private field -/
+/-! Structure with private field, imported -/
 /--
-info: structure Thunk.{u} : Type u → Type u
+info: structure Thunk.{u} (α : Type u) : Type u
 number of parameters: 1
-constructor:
-Thunk.mk : {α : Type u} → (Unit → α) → Thunk α
 fields:
-private fn : Unit → α
+  private Thunk.fn✝ : Unit → α
+constructor:
+  Thunk.mk.{u} {α : Type u} (fn : Unit → α) : Thunk α
 -/
 #guard_msgs in
 #print Thunk
 
-/- Extended class -/
+/-! Structure with private field, current module -/
+structure PrivField where
+  private x : Nat
+
 /--
-info: class Alternative.{u, v} : (Type u → Type v) → Type (max (u + 1) v)
-number of parameters: 1
-constructor:
-Alternative.mk : {f : Type u → Type v} →
-  [toApplicative : Applicative f] → ({α : Type u} → f α) → ({α : Type u} → f α → (Unit → f α) → f α) → Alternative f
+info: structure PrivField : Type
+number of parameters: 0
 fields:
-toApplicative : Applicative f
-failure : {α : Type u} → f α
-orElse : {α : Type u} → f α → (Unit → f α) → f α
+  private PrivField.x : Nat
+constructor:
+  PrivField.mk (x : Nat) : PrivField
+-/
+#guard_msgs in
+#print PrivField
+
+/-! Private constructor, imported -/
+/--
+info: class TypeName.{u} (α : Type u) : Type
+number of parameters: 1
+fields:
+  private TypeName.data✝ : (TypeNameData✝ α).type
+constructor:
+  private TypeName.mk'✝.{u} {α : Type u} (data : (TypeNameData✝ α).type) : TypeName α
+-/
+#guard_msgs in
+#print TypeName
+
+/-! Private constructor, current module -/
+structure PrivCtor where private mk ::
+  x : Nat
+/--
+info: structure PrivCtor : Type
+number of parameters: 0
+fields:
+  PrivCtor.x : Nat
+constructor:
+  private PrivCtor.mk (x : Nat) : PrivCtor
+-/
+#guard_msgs in
+#print PrivCtor
+
+/-! Extended class -/
+/--
+info: class Alternative.{u, v} (f : Type u → Type v) : Type (max (u + 1) v)
+number of parameters: 1
+parents:
+  Alternative.toApplicative : Applicative f
+fields:
+  Functor.map : {α β : Type u} → (α → β) → f α → f β
+  Functor.mapConst : {α β : Type u} → α → f β → f α
+  Pure.pure : {α : Type u} → α → f α
+  Seq.seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β
+  SeqLeft.seqLeft : {α β : Type u} → f α → (Unit → f β) → f α
+  SeqRight.seqRight : {α β : Type u} → f α → (Unit → f β) → f β
+  Alternative.failure : {α : Type u} → f α
+  Alternative.orElse : {α : Type u} → f α → (Unit → f α) → f α
+constructor:
+  Alternative.mk.{u, v} {f : Type u → Type v} [toApplicative : Applicative f] (failure : {α : Type u} → f α)
+    (orElse : {α : Type u} → f α → (Unit → f α) → f α) : Alternative f
+resolution order:
+  Alternative, Applicative, Functor, Pure, Seq, SeqLeft, SeqRight
 -/
 #guard_msgs in
 #print Alternative
 
-/- Multiply extended class -/
+/-! Multiply extended class -/
 /--
-info: class Applicative.{u, v} : (Type u → Type v) → Type (max (u + 1) v)
+info: class Applicative.{u, v} (f : Type u → Type v) : Type (max (u + 1) v)
 number of parameters: 1
-constructor:
-Applicative.mk : {f : Type u → Type v} →
-  [toFunctor : Functor f] →
-    [toPure : Pure f] → [toSeq : Seq f] → [toSeqLeft : SeqLeft f] → [toSeqRight : SeqRight f] → Applicative f
+parents:
+  Applicative.toFunctor : Functor f
+  Applicative.toPure : Pure f
+  Applicative.toSeq : Seq f
+  Applicative.toSeqLeft : SeqLeft f
+  Applicative.toSeqRight : SeqRight f
 fields:
-toFunctor : Functor f
-toPure : Pure f
-toSeq : Seq f
-toSeqLeft : SeqLeft f
-toSeqRight : SeqRight f
+  Functor.map : {α β : Type u} → (α → β) → f α → f β
+  Functor.mapConst : {α β : Type u} → α → f β → f α
+  Pure.pure : {α : Type u} → α → f α
+  Seq.seq : {α β : Type u} → f (α → β) → (Unit → f α) → f β
+  SeqLeft.seqLeft : {α β : Type u} → f α → (Unit → f β) → f α
+  SeqRight.seqRight : {α β : Type u} → f α → (Unit → f β) → f β
+constructor:
+  Applicative.mk.{u, v} {f : Type u → Type v} [toFunctor : Functor f] [toPure : Pure f] [toSeq : Seq f]
+    [toSeqLeft : SeqLeft f] [toSeqRight : SeqRight f] : Applicative f
+resolution order:
+  Applicative, Functor, Pure, Seq, SeqLeft, SeqRight
 -/
 #guard_msgs in
 #print Applicative
 
-/- Structure with unused parameter -/
+/-! Structure with unused parameter -/
 
 structure Weird (α β : Type _) where
   a : α
 
 /--
-info: structure Weird.{u_1, u_2} : Type u_1 → Type u_2 → Type u_1
+info: structure Weird.{u_1, u_2} (α : Type u_1) (β : Type u_2) : Type u_1
 number of parameters: 2
-constructor:
-Weird.mk : {α : Type u_1} → {β : Type u_2} → α → Weird α β
 fields:
-a : α
+  Weird.a : α
+constructor:
+  Weird.mk.{u_1, u_2} {α : Type u_1} {β : Type u_2} (a : α) : Weird α β
 -/
 #guard_msgs in
 #print Weird
 
-/- Structure-like inductive -/
+/-! Structure-like inductive -/
 
 inductive Fake (α : Type _) where
   | mk : (x : α) → Fake α
diff --git a/tests/lean/run/2291.lean b/tests/lean/run/2291.lean
index d3520cb313..e5330ac1d7 100644
--- a/tests/lean/run/2291.lean
+++ b/tests/lean/run/2291.lean
@@ -21,13 +21,13 @@ let _x_29 := Lean.Expr.const _x_28 _x_25;
 let _x_30 := _x_29.app _x_23;
 let _x_31 := [];
 let _x_32 := 0 :: _x_31;
-let _x_33 := Lean.List.toExprAux _x_27 _x_30 _x_32;
+let _x_33 := Lean.List.toExprAux✝ _x_27 _x_30 _x_32;
 Lean.MessageData.ofExpr _x_33
 [compiler.simp] >> _private.Lean.ToExpr.0.Lean.List.toExprAux._at._eval._spec_1
 fun nilFn consFn x =>
   List.casesOn fun head tail =>
     let _x_1 := Lean.mkNatLit head;
-    let _x_2 := Lean.List.toExprAux._at._eval._spec_1 nilFn consFn tail;
+    let _x_2 := Lean.List.toExprAux._at._eval._spec_1✝ nilFn consFn tail;
     Lean.mkAppB consFn _x_1 _x_2
 >> _eval
 let _x_14 := Lean.Name.str._override Lean.Name.anonymous._impl "Nat";
@@ -41,13 +41,13 @@ let _x_21 := `List.cons;
 let _x_22 := Lean.Expr.const._override _x_21 _x_18;
 let _x_23 := Lean.Expr.app._override _x_22 _x_16;
 let _x_24 := List.cons _neutral 0 _x_15;
-let _x_25 := Lean.List.toExprAux._at._eval._spec_1 _x_20 _x_23 _x_24;
+let _x_25 := Lean.List.toExprAux._at._eval._spec_1✝ _x_20 _x_23 _x_24;
 Lean.MessageData.ofExpr _x_25
 [compiler.simp] >> _private.Lean.ToExpr.0.Lean.List.toExprAux._at._eval._spec_1
 fun nilFn consFn x =>
   List.casesOn fun head tail =>
     let _x_1 := Lean.mkNatLit head;
-    let _x_2 := Lean.List.toExprAux._at._eval._spec_1 nilFn consFn tail;
+    let _x_2 := Lean.List.toExprAux._at._eval._spec_1✝ nilFn consFn tail;
     Lean.mkAppB consFn _x_1 _x_2
 >> _eval
 let _x_1 := Lean.Name.str._override Lean.Name.anonymous._impl "Nat";
@@ -61,13 +61,13 @@ let _x_8 := `List.cons;
 let _x_9 := Lean.Expr.const._override _x_8 _x_5;
 let _x_10 := Lean.Expr.app._override _x_9 _x_3;
 let _x_11 := List.cons _neutral 0 _x_2;
-let _x_12 := Lean.List.toExprAux._at._eval._spec_1 _x_7 _x_10 _x_11;
+let _x_12 := Lean.List.toExprAux._at._eval._spec_1✝ _x_7 _x_10 _x_11;
 Lean.MessageData.ofExpr _x_12
 [compiler.simp] >> _private.Lean.ToExpr.0.Lean.List.toExprAux._at._eval._spec_1
 fun nilFn consFn x =>
   List.casesOn fun head tail =>
     let _x_1 := Lean.mkNatLit head;
-    let _x_2 := Lean.List.toExprAux._at._eval._spec_1 nilFn consFn tail;
+    let _x_2 := Lean.List.toExprAux._at._eval._spec_1✝ nilFn consFn tail;
     Lean.mkAppB consFn _x_1 _x_2
 >> _eval._closed_1
 "Nat"
@@ -102,7 +102,7 @@ let _x_1 := List.nil _neutral;
 List.cons _neutral 0 _x_1
 >> _eval
 let _x_1 :=
-  Lean.List.toExprAux._at._eval._spec_1 _eval._closed_9 _eval._closed_13
+  Lean.List.toExprAux._at._eval._spec_1✝ _eval._closed_9 _eval._closed_13
     _eval._closed_14;
 Lean.MessageData.ofExpr _x_1
 ---
diff --git a/tests/lean/run/4465.lean b/tests/lean/run/4465.lean
index 94591e5dad..081b599642 100644
--- a/tests/lean/run/4465.lean
+++ b/tests/lean/run/4465.lean
@@ -3,7 +3,7 @@
 #reduce Char.ofNat (nat_lit 0)
 
 /--
-info: { val := { toBitVec := { toFin := ⟨0, isValidChar_UInt32 (Or.inl (Nat.le_of_ble_eq_true rfl))⟩ } },
+info: { val := { toBitVec := { toFin := ⟨0, isValidChar_UInt32✝ (Or.inl (Nat.le_of_ble_eq_true rfl))⟩ } },
   valid := Or.inl (Nat.le_of_ble_eq_true rfl) }
 -/
 #guard_msgs in
diff --git a/tests/lean/run/print_cmd.lean b/tests/lean/run/print_cmd.lean
index d59f9c2c43..65a21b21fa 100644
--- a/tests/lean/run/print_cmd.lean
+++ b/tests/lean/run/print_cmd.lean
@@ -2,18 +2,99 @@
 
 private def foo (x : Nat) : Nat := x + 1
 
-#print "hello"
-#print id
-#print propext
-#print default
-#print ReaderT.read
-#print Prod
-#print Prod.mk
-#print Nat
-#print Nat.succ
-#print Nat.rec
-#print Nat.casesOn
-#print foo
-#print Quot.mk
-#print Quot.ind
-#print Quot.mk
+/-- info: hello -/
+#guard_msgs in #print "hello"
+/--
+info: def id.{u} : {α : Sort u} → α → α :=
+fun {α} a => a
+-/
+#guard_msgs in #print id
+/-- info: axiom propext : ∀ {a b : Prop}, (a ↔ b) → a = b -/
+#guard_msgs in #print propext
+/--
+info: def Inhabited.default.{u} : {α : Sort u} → [self : Inhabited α] → α :=
+fun α [self : Inhabited α] => self.1
+-/
+#guard_msgs in #print default
+/--
+info: protected def ReaderT.read.{u, v} : {ρ : Type u} → {m : Type u → Type v} → [inst : Monad m] → ReaderT ρ m ρ :=
+fun {ρ} {m} [Monad m] => pure
+-/
+#guard_msgs in #print ReaderT.read
+/--
+info: structure Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)
+number of parameters: 2
+fields:
+  Prod.fst : α
+  Prod.snd : β
+constructor:
+  Prod.mk.{u, v} {α : Type u} {β : Type v} (fst : α) (snd : β) : α × β
+-/
+#guard_msgs in #print Prod
+/-- info: constructor Prod.mk.{u, v} : {α : Type u} → {β : Type v} → α → β → α × β -/
+#guard_msgs in #print Prod.mk
+/--
+info: inductive Nat : Type
+number of parameters: 0
+constructors:
+Nat.zero : Nat
+Nat.succ : Nat → Nat
+-/
+#guard_msgs in #print Nat
+/-- info: constructor Nat.succ : Nat → Nat -/
+#guard_msgs in #print Nat.succ
+/--
+info: recursor Nat.rec.{u} : {motive : Nat → Sort u} →
+  motive Nat.zero → ((n : Nat) → motive n → motive n.succ) → (t : Nat) → motive t
+-/
+#guard_msgs in #print Nat.rec
+/--
+info: @[reducible] def Nat.casesOn.{u} : {motive : Nat → Sort u} →
+  (t : Nat) → motive Nat.zero → ((n : Nat) → motive n.succ) → motive t :=
+fun {motive} t zero succ => Nat.rec zero (fun n n_ih => succ n) t
+-/
+#guard_msgs in #print Nat.casesOn
+/--
+info: private def foo : Nat → Nat :=
+fun x => x + 1
+-/
+#guard_msgs in #print foo
+/-- info: Quotient primitive Quot.mk.{u} : {α : Sort u} → (r : α → α → Prop) → α → Quot r -/
+#guard_msgs in #print Quot.mk
+/--
+info: Quotient primitive Quot.ind.{u} : ∀ {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop},
+  (∀ (a : α), β (Quot.mk r a)) → ∀ (q : Quot r), β q
+-/
+#guard_msgs in #print Quot.ind
+/-- info: Quotient primitive Quot.mk.{u} : {α : Sort u} → (r : α → α → Prop) → α → Quot r -/
+#guard_msgs in #print Quot.mk
+
+/-!
+Structure with diamond inheritance
+-/
+structure A where
+  a : Nat
+structure B extends A where
+  b : Nat
+structure C extends A where
+  c : Nat
+structure D extends B, C where
+  d : Nat
+
+/--
+info: structure D : Type
+number of parameters: 0
+parents:
+  D.toB : B
+  D.toC : C
+fields:
+  A.a : Nat
+  B.b : Nat
+  C.c : Nat
+  D.d : Nat
+constructor:
+  D.mk (toB : B) (c d : Nat) : D
+resolution order:
+  D, B, C, A
+-/
+#guard_msgs in #print D
diff --git a/tests/lean/structAutoBound.lean.expected.out b/tests/lean/structAutoBound.lean.expected.out
index 85f9426ef2..6c66d7380c 100644
--- a/tests/lean/structAutoBound.lean.expected.out
+++ b/tests/lean/structAutoBound.lean.expected.out
@@ -1,16 +1,16 @@
-structure Foo.{v, u_1} : {α : Sort u_1} → (α → Type v) → Sort (max u_1 (v + 1))
+structure Foo.{v, u_1} {α : Sort u_1} (β : α → Type v) : Sort (max u_1 (v + 1))
 number of parameters: 2
-constructor:
-Foo.mk : {α : Sort u_1} → {β : α → Type v} → (a : α) → β a → Foo β
 fields:
-a : α
-b : β self.a
+  Foo.a : α
+  Foo.b : β self.a
+constructor:
+  Foo.mk.{v, u_1} {α : Sort u_1} {β : α → Type v} (a : α) (b : β a) : Foo β
 structAutoBound.lean:9:15-9:16: error: a universe level named 'u' has already been declared
-structure Boo.{u, v} : Type u → Type v → Type (max u v)
+structure Boo.{u, v} (α : Type u) (β : Type v) : Type (max u v)
 number of parameters: 2
-constructor:
-Boo.mk : {α : Type u} → {β : Type v} → α → β → Boo α β
 fields:
-a : α
-b : β
+  Boo.a : α
+  Boo.b : β
+constructor:
+  Boo.mk.{u, v} {α : Type u} {β : Type v} (a : α) (b : β) : Boo α β
 structAutoBound.lean:18:10-18:44: error: unused universe parameter 'w'