diff options
| author | Emilio Jesus Gallego Arias | 2020-02-21 16:24:41 -0500 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-02-21 16:24:41 -0500 |
| commit | 6aa5057f98c0196a5897ca82699125a5a16bf22b (patch) | |
| tree | 4acbaa40e0ea45faef61b0b26bed590a3980fbd9 | |
| parent | c45b7e41a1caa4d5ec4785c2bf323bdd11ad8d2e (diff) | |
| parent | fc9fa470c35f3716d0d49af182f02925b060286d (diff) | |
Merge PR #11642: Unconditionally print explanation for universe inconsistencies
Reviewed-by: ejgallego
| -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 |