diff options
| author | Gaëtan Gilbert | 2020-02-20 16:34:49 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-20 16:34:49 +0100 |
| commit | fc9fa470c35f3716d0d49af182f02925b060286d (patch) | |
| tree | 2b32a07860cb08d4d26cafd88ee1a71d9e906bd7 /vernac/himsg.ml | |
| parent | 21551b37cfa25657cf51179ad60e9ead455390f0 (diff) | |
Unconditionally print explanation for universe inconsistencies
ie regardless of the Print Universes flag.
AFAICT there is no point in skipping them.
Diffstat (limited to 'vernac/himsg.ml')
| -rw-r--r-- | vernac/himsg.ml | 16 |
1 files changed, 4 insertions, 12 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index dfc4631572..f6f6c4f1eb 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -324,11 +324,8 @@ let explain_unification_error env sigma p1 p2 = function strbrk ": cannot ensure that " ++ t ++ strbrk " is a subtype of " ++ u] | UnifUnivInconsistency p -> - if !Constrextern.print_universes then - [str "universe inconsistency: " ++ - Univ.explain_universe_inconsistency (Termops.pr_evd_level sigma) p] - else - [str "universe inconsistency"] + [str "universe inconsistency: " ++ + Univ.explain_universe_inconsistency (Termops.pr_evd_level sigma) p] | CannotSolveConstraint ((pb,env,t,u),e) -> let env = make_all_name_different env sigma in (strbrk "cannot satisfy constraint " ++ pr_leconstr_env env sigma t ++ @@ -1375,13 +1372,8 @@ let _ = CErrors.register_handler explain_exn_default let rec vernac_interp_error_handler = function | Univ.UniverseInconsistency i -> - let msg = - if !Constrextern.print_universes then - str "." ++ spc() ++ - Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i - else - mt() in - str "Universe inconsistency" ++ msg ++ str "." + str "Universe inconsistency." ++ spc() ++ + Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes i ++ str "." | TypeError(ctx,te) -> let te = map_ptype_error EConstr.of_constr te in explain_type_error ctx Evd.empty te |