diff options
Diffstat (limited to 'kernel/subtyping.ml')
| -rw-r--r-- | kernel/subtyping.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index e5b81c72f..99c1b8483 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -219,7 +219,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let check_conv cst f = check_conv_error error cst f in let check_type cst env t1 t2 = - let err = NotConvertibleTypeField (t1, t2) in + let err = NotConvertibleTypeField (env, t1, t2) in (* If the type of a constant is generated, it may mention non-variable algebraic universes that the general conversion @@ -303,7 +303,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = if Declareops.constant_has_body cb2 then error DefinitionFieldExpected; let arity1 = type_of_inductive env (mind1,mind1.mind_packets.(i)) in let typ2 = Typeops.type_of_constant_type env cb2.const_type in - let error = NotConvertibleTypeField (arity1, typ2) in + let error = NotConvertibleTypeField (env, arity1, typ2) in check_conv error cst conv_leq env arity1 typ2 | IndConstr (((kn,i),j) as cstr,mind1) -> ignore (Errors.error ( @@ -315,7 +315,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = if Declareops.constant_has_body cb2 then error DefinitionFieldExpected; let ty1 = type_of_constructor cstr (mind1,mind1.mind_packets.(i)) in let ty2 = Typeops.type_of_constant_type env cb2.const_type in - let error = NotConvertibleTypeField (ty1, ty2) in + let error = NotConvertibleTypeField (env, ty1, ty2) in check_conv error cst conv env ty1 ty2 let rec check_modules cst env msb1 msb2 subst1 subst2 = |