diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /checker/subtyping.ml | |
parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) |
Imported Upstream version 8.6upstream/8.6
Diffstat (limited to 'checker/subtyping.ml')
-rw-r--r-- | checker/subtyping.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/checker/subtyping.ml b/checker/subtyping.ml index e4192257..7eae9b83 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -7,7 +7,7 @@ (************************************************************************) (*i*) -open Errors +open CErrors open Util open Names open Cic @@ -103,7 +103,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= in let eq_projection_body p1 p2 = let check eq f = if not (eq (f p1) (f p2)) then error () in - check eq_mind (fun x -> x.proj_ind); + check MutInd.equal (fun x -> x.proj_ind); check (==) (fun x -> x.proj_npars); check (==) (fun x -> x.proj_arg); check (eq_constr) (fun x -> x.proj_type); @@ -302,7 +302,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let c2 = force_constr lc2 in check_conv conv env c1 c2)) | IndType ((kn,i),mind1) -> - ignore (Errors.error ( + ignore (CErrors.error ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ @@ -313,7 +313,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let typ2 = Typeops.type_of_constant_type env cb2.const_type in check_conv conv_leq env arity1 typ2 | IndConstr (((kn,i),j) as cstr,mind1) -> - ignore (Errors.error ( + ignore (CErrors.error ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by a constructor. Hint: you can rename the " ^ "constructor and give a definition to map the old name to the new " ^ |