diff options
| author | Matthieu Sozeau | 2014-08-07 14:08:29 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-08-13 11:52:38 +0200 |
| commit | bcb425ead1d12d6e800f9f13f28b34da529c463e (patch) | |
| tree | b32572d718d3c7bec77c64742f5ddf6e6989b893 | |
| parent | c7480636bce632adfa28d6bb0b423a086ade4318 (diff) | |
Bettre pretty-printing of evar maps, avoids printing universe information
for typeclass errors.
| -rw-r--r-- | pretyping/evd.ml | 14 | ||||
| -rw-r--r-- | pretyping/evd.mli | 4 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 2 |
3 files changed, 10 insertions, 10 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index fcc58f43fd..ff04bda809 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1617,10 +1617,10 @@ let pr_evar_constraints pbs = in prlist_with_sep fnl pr_evconstr pbs -let pr_evar_map_gen pr_evars sigma = +let pr_evar_map_gen with_univs pr_evars sigma = let { universes = uvs } = sigma in - let evs = if has_no_evar sigma then mt () else pr_evars sigma - and svs = pr_evar_universe_context uvs + let evs = if has_no_evar sigma then mt () else pr_evars sigma ++ fnl () + and svs = if with_univs then pr_evar_universe_context uvs else mt () and cstrs = if List.is_empty sigma.conv_pbs then mt () else @@ -1666,11 +1666,11 @@ let pr_evar_by_filter filter sigma = in prdef ++ prundef -let pr_evar_map depth sigma = - pr_evar_map_gen (fun sigma -> pr_evar_by_depth depth sigma) sigma +let pr_evar_map ?(with_univs=true) depth sigma = + pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_depth depth sigma) sigma -let pr_evar_map_filter filter sigma = - pr_evar_map_gen (fun sigma -> pr_evar_by_filter filter sigma) sigma +let pr_evar_map_filter ?(with_univs=true) filter sigma = + pr_evar_map_gen with_univs (fun sigma -> pr_evar_by_filter filter sigma) sigma let pr_metaset metas = str "[" ++ pr_sequence pr_meta (Metaset.elements metas) ++ str "]" diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 5aa8a13d70..28e978edf1 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -517,8 +517,8 @@ type unsolvability_explanation = SeveralInstancesFound of int val pr_evar_info : evar_info -> Pp.std_ppcmds val pr_evar_constraints : evar_constraint list -> Pp.std_ppcmds -val pr_evar_map : int option -> evar_map -> Pp.std_ppcmds -val pr_evar_map_filter : (Evar.t -> evar_info -> bool) -> +val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.std_ppcmds +val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) -> evar_map -> Pp.std_ppcmds val pr_metaset : Metaset.t -> Pp.std_ppcmds val pr_evar_universe_context : evar_universe_context -> Pp.std_ppcmds diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 7497393e5d..4e3d460ded 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 |