diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/type_errors.ml | 4 | ||||
| -rw-r--r-- | kernel/type_errors.mli | 4 | ||||
| -rw-r--r-- | kernel/typeops.ml | 18 | ||||
| -rw-r--r-- | kernel/typeops.mli | 2 |
4 files changed, 14 insertions, 14 deletions
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index c2cdf98ee8..6c06c1e0f1 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -48,7 +48,7 @@ type ('constr, 'types) ptype_error = | UnboundVar of variable | NotAType of ('constr, 'types) punsafe_judgment | BadAssumption of ('constr, 'types) punsafe_judgment - | ReferenceVariables of Id.t * 'constr + | ReferenceVariables of Id.t * GlobRef.t | ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment * (Sorts.family * Sorts.family * Sorts.family * arity_error) option | CaseNotInductive of ('constr, 'types) punsafe_judgment @@ -182,7 +182,7 @@ let map_ptype_error f = function | UnboundVar id -> UnboundVar id | NotAType j -> NotAType (on_judgment f j) | BadAssumption j -> BadAssumption (on_judgment f j) -| ReferenceVariables (id, c) -> ReferenceVariables (id, f c) +| ReferenceVariables (id, c) -> ReferenceVariables (id, c) | ElimArity (pi, c, j, ar) -> ElimArity (pi, f c, on_judgment f j, ar) | CaseNotInductive j -> CaseNotInductive (on_judgment f j) | WrongCaseInfo (pi, ci) -> WrongCaseInfo (pi, ci) diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 0f29717f12..d9842ecefa 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -49,7 +49,7 @@ type ('constr, 'types) ptype_error = | UnboundVar of variable | NotAType of ('constr, 'types) punsafe_judgment | BadAssumption of ('constr, 'types) punsafe_judgment - | ReferenceVariables of Id.t * 'constr + | ReferenceVariables of Id.t * GlobRef.t | ElimArity of pinductive * 'constr * ('constr, 'types) punsafe_judgment * (Sorts.family * Sorts.family * Sorts.family * arity_error) option | CaseNotInductive of ('constr, 'types) punsafe_judgment @@ -102,7 +102,7 @@ val error_not_type : env -> unsafe_judgment -> 'a val error_assumption : env -> unsafe_judgment -> 'a -val error_reference_variables : env -> Id.t -> constr -> 'a +val error_reference_variables : env -> Id.t -> GlobRef.t -> 'a val error_elim_arity : env -> pinductive -> constr -> unsafe_judgment -> diff --git a/kernel/typeops.ml b/kernel/typeops.ml index c74bfd0688..2a35f87db8 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -116,7 +116,7 @@ let type_of_variable env id = (* Checks if a context of variables can be instantiated by the variables of the current env. Order does not have to be checked assuming that all names are distinct *) -let check_hyps_inclusion env ?evars f c sign = +let check_hyps_inclusion env ?evars c sign = let conv env a b = conv env ?evars a b in Context.Named.fold_outside (fun d1 () -> @@ -133,7 +133,7 @@ let check_hyps_inclusion env ?evars f c sign = | LocalDef _, LocalAssum _ -> raise NotConvertible | LocalDef (_,b2,_), LocalDef (_,b1,_) -> conv env b2 b1); with Not_found | NotConvertible | Option.Heterogeneous -> - error_reference_variables env id (f c)) + error_reference_variables env id c) sign ~init:() @@ -146,14 +146,14 @@ let check_hyps_inclusion env ?evars f c sign = let type_of_constant env (kn,_u as cst) = let cb = lookup_constant kn env in - let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in + let () = check_hyps_inclusion env (GlobRef.ConstRef kn) cb.const_hyps in let ty, cu = constant_type env cst in let () = check_constraints cu env in ty let type_of_constant_in env (kn,_u as cst) = let cb = lookup_constant kn env in - let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in + let () = check_hyps_inclusion env (GlobRef.ConstRef kn) cb.const_hyps in constant_type_in env cst (* Type of a lambda-abstraction. *) @@ -368,18 +368,18 @@ let check_cast env c ct k expected_type = the App case of execute; from this constraints, the expected dynamic constraints of the form u<=v are enforced *) -let type_of_inductive_knowing_parameters env (ind,u as indu) args = +let type_of_inductive_knowing_parameters env (ind,u) args = let (mib,_mip) as spec = lookup_mind_specif env ind in - check_hyps_inclusion env mkIndU indu mib.mind_hyps; + check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps; let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters env (spec,u) args in check_constraints cst env; t -let type_of_inductive env (ind,u as indu) = +let type_of_inductive env (ind,u) = let (mib,mip) = lookup_mind_specif env ind in - check_hyps_inclusion env mkIndU indu mib.mind_hyps; + check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps; let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in check_constraints cst env; t @@ -390,7 +390,7 @@ let type_of_constructor env (c,_u as cu) = let () = let ((kn,_),_) = c in let mib = lookup_mind kn env in - check_hyps_inclusion env mkConstructU cu mib.mind_hyps + check_hyps_inclusion env (GlobRef.ConstructRef c) mib.mind_hyps in let specif = lookup_mind_specif env (inductive_of_constructor c) in let t,cst = constrained_type_of_constructor cu specif in diff --git a/kernel/typeops.mli b/kernel/typeops.mli index ae816fe26e..f88bc653de 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -111,7 +111,7 @@ val type_of_global_in_context : env -> GlobRef.t -> types * Univ.AUContext.t (** Check that hyps are included in env and fails with error otherwise *) val check_hyps_inclusion : env -> ?evars:((existential->constr option) * UGraph.t) -> - ('a -> constr) -> 'a -> Constr.named_context -> unit + GlobRef.t -> Constr.named_context -> unit val check_primitive_type : env -> CPrimitives.op_or_type -> types -> unit |