From 250afa5b896a7e8ab5971667e6889ee3a498dfd3 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 22 Nov 2014 17:16:23 +0100 Subject: Removing superfluous newlines in setoid_rewrite error message. --- toplevel/himsg.ml | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 44e98a513..421a975f1 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -701,16 +701,15 @@ let pr_constraints printenv env sigma evars cstrs = let env' = reset_with_named_context evi.evar_hyps env in let pe = if printenv then - pr_ne_context_of (str "In environment:") (mt ()) - env' sigma ++ fnl () + pr_ne_context_of (str "In environment:") (mt ()) env' sigma else mt () in let evs = - prlist_with_sep (fun () -> fnl ()) - (fun (ev, evi) -> pr_existential_key sigma ev ++ + prlist + (fun (ev, evi) -> fnl () ++ pr_existential_key sigma ev ++ str " : " ++ pr_lconstr_env env' sigma evi.evar_concl) l in - pe ++ evs ++ fnl() ++ h 0 (pr_evar_constraints cstrs) + h 0 (pe ++ evs ++ pr_evar_constraints cstrs) else let filter evk _ = Evar.Map.mem evk evars in pr_evar_map_filter ~with_univs:false filter sigma -- cgit v1.2.3