diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/modops.ml | 2 | ||||
| -rw-r--r-- | kernel/modops.mli | 2 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 6 |
3 files changed, 5 insertions, 5 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index c1b5d788d3..6c46ad5103 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -33,7 +33,7 @@ type signature_mismatch_error = | NotConvertibleInductiveField of Id.t | NotConvertibleConstructorField of Id.t | NotConvertibleBodyField - | NotConvertibleTypeField of types * types + | NotConvertibleTypeField of env * types * types | NotSameConstructorNamesField | NotSameInductiveNameInBlockField | FiniteInductiveFieldExpected of bool diff --git a/kernel/modops.mli b/kernel/modops.mli index 600e631a7c..66aadd124c 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -60,7 +60,7 @@ type signature_mismatch_error = | NotConvertibleInductiveField of Id.t | NotConvertibleConstructorField of Id.t | NotConvertibleBodyField - | NotConvertibleTypeField of types * types + | NotConvertibleTypeField of env * types * types | NotSameConstructorNamesField | NotSameInductiveNameInBlockField | FiniteInductiveFieldExpected of bool diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index e5b81c72f6..99c1b8483e 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 = |