aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/himsg.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/himsg.ml')
-rw-r--r--toplevel/himsg.ml9
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