diff options
| author | Maxime Dénès | 2019-05-24 14:08:04 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-05-27 09:21:31 +0200 |
| commit | 7d732b9472908cfb6b444e936f842613d55e1e7d (patch) | |
| tree | c3b9292fd5c2f020f2be287ee31349be00d47781 /engine | |
| parent | 4e324a95217bedae198360d1078e3b664fb2deea (diff) | |
[debug] Print restriction metadata in evar map debug printer
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/termops.ml | 6 |
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 ())) |
