diff --git a/printing/printer.ml b/printing/printer.ml
index 99d0cea7a16a..7b10f6a6d963 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -741,7 +741,9 @@ let process_dependent_evar q acc evm is_dependent e =
   let () = match Evd.evar_body evi with
   | Evar_empty ->
     queue_term q true (Evd.evar_concl evi)
-  | Evar_defined b -> ()
+  | Evar_defined b ->
+    let env = Evd.evar_filtered_env (Global.env ()) evi in
+    queue_term q true (Retyping.get_type_of env evm b)
   in
   List.iter begin fun decl ->
     let open NamedDecl in
diff --git a/test-suite/output-coqtop/DependentEvars3.out b/test-suite/output-coqtop/DependentEvars3.out
new file mode 100644
index 000000000000..cbcf062fa510
--- /dev/null
+++ b/test-suite/output-coqtop/DependentEvars3.out
@@ -0,0 +1,41 @@
+
+Coq < 
+Coq < 1 goal
+  
+  ============================
+  (exists n : nat, n = 5 \/ True) /\ (exists m : nat, m = 6 \/ True)
+
+(dependent evars: ; in current goal:)
+
+x < 
+x < 2 goals
+  
+  ============================
+  exists n : nat, n = 5 \/ True
+
+goal 2 is:
+ exists m : nat, m = 6 \/ True
+
+(dependent evars: ; in current goal:)
+
+x < 2 focused goals (shelved: 1)
+  
+  ============================
+  ?n = 5 \/ True
+
+goal 2 is:
+ exists m : nat, m = 6 \/ True
+
+(dependent evars: ?X10:?n; in current goal: ?X10)
+
+x < 2 focused goals (shelved: 1)
+  
+  ============================
+  True
+
+goal 2 is:
+ exists m : nat, m = 6 \/ True
+
+(dependent evars: ?X10:?n; in current goal:)
+
+x < 
diff --git a/test-suite/output-coqtop/DependentEvars3.v b/test-suite/output-coqtop/DependentEvars3.v
new file mode 100644
index 000000000000..af236bb6ff98
--- /dev/null
+++ b/test-suite/output-coqtop/DependentEvars3.v
@@ -0,0 +1,6 @@
+Set Printing Dependent Evars Line.
+Lemma x : (exists(n : nat), n = 5 \/ True) /\ (exists(m : nat), m = 6 \/ True).
+Proof using.
+  split.
+    eexists.
+    right.