diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-05 14:21:01 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-05 17:55:32 +0100 |
| commit | e4f9b2a8af4489b9d7fb27dcd2f919a54491c402 (patch) | |
| tree | 4c4385c112179082bd5b2a8a315f847b65c163b1 /pretyping/evd.ml | |
| parent | 8bf7221667dc2868027ed1080b3b70fd66144309 (diff) | |
More consistent printing of evars in evar_map debugging printer.
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 933684143..1d05d6c6e 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -128,7 +128,7 @@ module Store = Store.Make(Dummy) type evar = Term.existential_key -let string_of_existential evk = "?" ^ string_of_int (Evar.repr evk) +let string_of_existential evk = "?X" ^ string_of_int (Evar.repr evk) type evar_body = | Evar_empty @@ -1740,7 +1740,9 @@ let pr_evar_list sigma l = let pr (ev, evi) = h 0 (str (string_of_existential ev) ++ str "==" ++ pr_evar_info evi ++ - str " {" ++ pr_id (evar_ident ev sigma) ++ str "}") + (if evi.evar_body == Evar_empty + then str " {" ++ pr_id (evar_ident ev sigma) ++ str "}" + else mt ())) in h 0 (prlist_with_sep fnl pr l) |