From 411973d14a95b043f93ed6d0ca628a6a98e3c221 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 18 Aug 2016 22:32:59 +0200 Subject: [checker] Fix/fine tune printing. In 91ee24b4a7843793a84950379277d92992ba1651 , we discouraged direct access to the console, recommending instead to provide information to the user by means of the `Feedback.msg_*` facilities. However, we introduced a display bug in the checker printer as it is special and doesn't use the Pp facilities (likely for trust reasons), spotted by @herbelin This patch fixes this bug and performs a couple more of fine tunings in the input. However, it could be desirable to port the `checker/printer.ml` to `Pp` and use the feedback mechanism; this would allow IDEs to use the checker in a more convenient way, at the cost of trusting `Pp` (which is already a bit trusted currently) A start of that idea can be found at: https://github.com/ejgallego/coq/tree/fix_checker_printing --- checker/checker.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'checker/checker.ml') diff --git a/checker/checker.ml b/checker/checker.ml index 0c411ae44..a7c45b824 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -16,6 +16,8 @@ open Check let () = at_exit flush_all +let chk_pp = Pp.pp_with Format.std_formatter + let fatal_error info anomaly = flush_all (); Feedback.msg_error info; flush_all (); exit (if anomaly then 129 else 1) @@ -282,7 +284,8 @@ let rec explain_exn = function Format.printf "@\nis not convertible with@\n"; Print.print_pure_constr a; Format.printf "@\n====== universes ====@\n"; - Feedback.msg_notice (Univ.pr_universes + chk_pp + (Univ.pr_universes (ctx.Environ.env_stratification.Environ.env_universes)); str "\nCantApplyBadType at argument " ++ int n | CantApplyNonFunctional _ -> str"CantApplyNonFunctional" -- cgit v1.2.3