diff options
Diffstat (limited to 'kernel/type_errors.ml')
| -rw-r--r-- | kernel/type_errors.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 624604976e..bcb7aa88ca 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -69,7 +69,7 @@ type ('constr, 'types) ptype_error = | DisallowedSProp | BadRelevance | BadInvert - | BadVariance of Level.t + | BadVariance of { lev : Level.t; expected : Variance.t; actual : Variance.t } type type_error = (constr, types) ptype_error @@ -164,8 +164,8 @@ let error_bad_relevance env = let error_bad_invert env = raise (TypeError (env, BadInvert)) -let error_bad_variance env u = - raise (TypeError (env, BadVariance u)) +let error_bad_variance env ~lev ~expected ~actual = + raise (TypeError (env, BadVariance {lev;expected;actual})) let map_pguard_error f = function | NotEnoughAbstractionInFixBody -> NotEnoughAbstractionInFixBody |