From 19d89158f4e0e4be5998f2ff9b64e90270977a32 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 5 Mar 2011 16:42:42 +0000 Subject: Moving printing of module typing errors upwards to himsg.ml so as to be able to call term printers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13886 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/subtyping.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'kernel/subtyping.ml') diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 8085575217..0c72995080 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -78,7 +78,7 @@ let check_conv_error error why cst f env a1 a2 = let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2= let kn1 = make_mind mp1 empty_dirpath l in let kn2 = make_mind mp2 empty_dirpath l in - let error why = error_not_match l spec2 why in + let error why = error_signature_mismatch l spec2 why in let check_conv why cst f = check_conv_error error why cst f in let mib1 = match info1 with @@ -201,7 +201,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = - let error why = error_not_match l spec2 why in + let error why = error_signature_mismatch l spec2 why in let check_conv cst f = check_conv_error error cst f in let check_type cst env t1 t2 = @@ -353,13 +353,13 @@ and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2= match info1 with | Module msb -> check_modules cst env msb msb2 subst1 subst2 - | _ -> error_not_match l spec2 ModuleFieldExpected + | _ -> error_signature_mismatch l spec2 ModuleFieldExpected end | SFBmodtype mtb2 -> let mtb1 = match info1 with | Modtype mtb -> mtb - | _ -> error_not_match l spec2 ModuleTypeFieldExpected + | _ -> error_signature_mismatch l spec2 ModuleTypeFieldExpected in let env = add_module (module_body_of_type mtb2.typ_mp mtb2) (add_module (module_body_of_type mtb1.typ_mp mtb1) env) in -- cgit v1.2.3