diff options
| author | Gaëtan Gilbert | 2020-11-16 17:38:33 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-11-16 17:58:56 +0100 |
| commit | f3c24a6246249db25bcc5c4a3e34040a8667ca02 (patch) | |
| tree | 86eedf85f4abc0a530646ef2168642e69928e933 /vernac/himsg.ml | |
| parent | 19f7d82edd68fb8940c7bcd73a229e957dee260c (diff) | |
Improve bad variance error message: mention expected and actual variances
Diffstat (limited to 'vernac/himsg.ml')
| -rw-r--r-- | vernac/himsg.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index c4f7e77714..9d86ea90e6 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -744,8 +744,10 @@ let explain_bad_relevance env = let explain_bad_invert env = strbrk "Bad case inversion (maybe a bugged tactic)." -let explain_bad_variance env sigma u = - str "Incorrect variance for universe " ++ Termops.pr_evd_level sigma u ++ str"." +let explain_bad_variance env sigma ~lev ~expected ~actual = + str "Incorrect variance for universe " ++ Termops.pr_evd_level sigma lev ++ + str": expected " ++ Univ.Variance.pr expected ++ + str " but cannot be less restrictive than " ++ Univ.Variance.pr actual ++ str "." let explain_type_error env sigma err = let env = make_all_name_different env sigma in @@ -791,7 +793,7 @@ let explain_type_error env sigma err = | DisallowedSProp -> explain_disallowed_sprop () | BadRelevance -> explain_bad_relevance env | BadInvert -> explain_bad_invert env - | BadVariance u -> explain_bad_variance env sigma u + | BadVariance {lev;expected;actual} -> explain_bad_variance env sigma ~lev ~expected ~actual let pr_position (cl,pos) = let clpos = match cl with |