diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2016-09-30 10:19:38 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2016-09-30 10:19:38 +0200 |
| commit | 1b2d1628dfa52e6c1a5a0c328b80829b03cea58f (patch) | |
| tree | 60a8ef4c90db2c3552abdd2882482daa7948034c /checker/checker.ml | |
| parent | 916d5fcc32f5110f23b60b21489d89598e6b8674 (diff) | |
| parent | 411973d14a95b043f93ed6d0ca628a6a98e3c221 (diff) | |
Merge remote-tracking branch 'github/pr/257' into v8.6
Was PR#257: [checker] Fix/fine tune printing.
Diffstat (limited to 'checker/checker.ml')
| -rw-r--r-- | checker/checker.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/checker/checker.ml b/checker/checker.ml index 503697b59..8dbb7e011 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) @@ -283,7 +285,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" |