diff options
Diffstat (limited to 'vernac/vernacentries.ml')
-rw-r--r-- | vernac/vernacentries.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index f0e41d27c..eae8167c4 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1741,7 +1741,7 @@ let vernac_print ~atts env sigma = else str"There may remain asynchronous universe constraints" in begin match dst with - | None -> UGraph.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining + | None -> UGraph.pr_universes UnivNames.pr_with_global_universes univ ++ pr_remaining | Some s -> dump_universes_gen univ s end | PrintHint r -> Hints.pr_hint_ref env sigma (smart_global r) @@ -2243,7 +2243,7 @@ let with_fail st b f = | HasNotFailed -> user_err ~hdr:"Fail" (str "The command has not failed!") | HasFailed msg -> - if not !Flags.quiet || !Flags.test_mode || !Flags.ide_slave then Feedback.msg_info + if not !Flags.quiet || !Flags.test_mode then Feedback.msg_info (str "The command has indeed failed with message:" ++ fnl () ++ msg) | _ -> assert false end |