From 04105f0430cad4e8d018ab47efccf79bf8511a32 Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Thu, 4 Jul 2019 23:19:10 -0700
Subject: Fix #10420 Add dependent evar mapping info to output

---
 toplevel/coqloop.ml | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 07466d641e..1f319d2bfd 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -405,7 +405,17 @@ let rec vernac_loop ~state =
 
     | Some (VernacShowGoal {gid; sid}) ->
       let proof = Stm.get_proof ~doc:state.doc (Stateid.of_int sid) in
-      Feedback.msg_notice (Printer.pr_goal_emacs ~proof gid sid);
+      let goal = Printer.pr_goal_emacs ~proof gid sid in
+      let evars =
+        match proof with
+        | None -> mt()
+        | Some p ->
+          let gl = (Evar.unsafe_of_int gid) in
+          let { Proof.sigma } = Proof.data p in
+          try Printer.print_dependent_evars (Some gl) sigma [ gl ]
+          with Not_found -> mt()
+      in
+      Feedback.msg_notice (v 0 (goal ++ evars));
       vernac_loop ~state
 
     | None ->
-- 
cgit v1.2.3