From d1dc6347fb9aa0659f8a8e824c33937d6bfb6e3e Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 28 Aug 2020 16:39:18 +0200
Subject: Enrich `evar_map` printer with future goals stack

This is a useful for debugging.
---
 engine/termops.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index e5231ef9cd..7579631313 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -301,8 +301,10 @@ let pr_evar_map_gen with_univs pr_evars env sigma =
     if List.is_empty (Evd.meta_list sigma) then mt ()
     else
       str "METAS:" ++ brk (0, 1) ++ pr_meta_map env sigma
+  and future_goals =
+    str "FUTURE GOALS STACK:" ++ brk (0, 1) ++ Evd.pr_future_goals_stack sigma ++ fnl ()
   in
-  evs ++ svs ++ cstrs ++ typeclasses ++ obligations ++ metas
+  evs ++ svs ++ cstrs ++ typeclasses ++ obligations ++ metas ++ future_goals
 
 let pr_evar_list env sigma l =
   let open Evd in
-- 
cgit v1.2.3