aboutsummaryrefslogtreecommitdiff
path: root/engine/termops.ml
diff options
context:
space:
mode:
authorMaxime Dénès2019-05-24 14:08:04 +0200
committerMaxime Dénès2019-05-27 09:21:31 +0200
commit7d732b9472908cfb6b444e936f842613d55e1e7d (patch)
treec3b9292fd5c2f020f2be287ee31349be00d47781 /engine/termops.ml
parent4e324a95217bedae198360d1078e3b664fb2deea (diff)
[debug] Print restriction metadata in evar map debug printer
Diffstat (limited to 'engine/termops.ml')
-rw-r--r--engine/termops.ml6
1 files changed, 6 insertions, 0 deletions
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 ()))