From 995177d90ea4d5649717bbfcd5c83d8a7bda3760 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= <gaetan.gilbert@skyskimmer.net>
Date: Mon, 13 Jan 2025 14:39:13 +0100
Subject: [PATCH] Fix debug printer on binder with evars

---
 engine/namegen.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/engine/namegen.ml b/engine/namegen.ml
index c27d3bef367f..96bd62aae6c7 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -522,7 +522,11 @@ let next_name_for_display gen env sigma flags na avoid =
 
 (* Remark: Anonymous var may be dependent in Evar's contexts *)
 let compute_displayed_name_in_gen_poly gen noccurn_fun env sigma flags avoid na c =
-  if noccurn_fun sigma 1 c then Anonymous, avoid
+  let noccurs =
+    try noccurn_fun sigma 1 c
+    with _ when !Flags.in_debugger -> false
+  in
+  if noccurs then Anonymous, avoid
   else
     let fresh_id, avoid = next_name_for_display gen env sigma flags na avoid in
     Name fresh_id, avoid