diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-22 17:16:23 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-11-22 19:23:32 +0100 |
| commit | 250afa5b896a7e8ab5971667e6889ee3a498dfd3 (patch) | |
| tree | d20c1083a60ce6ea92db2aa5f73fda4a84af3051 | |
| parent | 93c7fc0e58c8d510392b6ef95d9196e92925edb4 (diff) | |
Removing superfluous newlines in setoid_rewrite error message.
| -rw-r--r-- | toplevel/himsg.ml | 9 |
1 files 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 |