From 7d732b9472908cfb6b444e936f842613d55e1e7d Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 24 May 2019 14:08:04 +0200
Subject: [debug] Print restriction metadata in evar map debug printer

---
 engine/termops.ml | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'engine/termops.ml')

diff --git a/engine/termops.ml b/engine/termops.ml
index fcacb53ac4..05bb42ac61 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -306,9 +306,15 @@ let pr_evar_map_gen with_univs pr_evars env sigma =
 
 let pr_evar_list env sigma l =
   let open Evd in
+  let pr_restrict ev =
+    match is_restricted_evar sigma ev with
+    | None -> mt ()
+    | Some ev' -> str " (restricted to " ++ Evar.print ev' ++ str ")"
+  in
   let pr (ev, evi) =
     h 0 (Evar.print ev ++
       str "==" ++ pr_evar_info env sigma evi ++
+      pr_restrict ev ++
       (if evi.evar_body == Evar_empty
        then str " {" ++ pr_existential_key sigma ev ++ str "}"
        else mt ()))
-- 
cgit v1.2.3