diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-08-07 14:08:29 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-08-13 11:52:38 +0200 |
| commit | bcb425ead1d12d6e800f9f13f28b34da529c463e (patch) | |
| tree | b32572d718d3c7bec77c64742f5ddf6e6989b893 /toplevel | |
| parent | c7480636bce632adfa28d6bb0b423a086ade4318 (diff) | |
Bettre pretty-printing of evar maps, avoids printing universe information
for typeclass errors.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 7497393e5..4e3d460de 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -875,7 +875,7 @@ let pr_constraints printenv env evd evars cstrs = pe ++ evs ++ fnl() ++ h 0 (pr_evar_constraints cstrs) else let filter evk _ = Evar.Map.mem evk evars in - pr_evar_map_filter filter evd + pr_evar_map_filter ~with_univs:false filter evd let explain_unsatisfiable_constraints env evd constr comp = let (_, constraints) = Evd.extract_all_conv_pbs evd in |