diff options
| -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 | ||||
| -rw-r--r-- | pretyping/inductiveops.ml | 4 | ||||
| -rw-r--r-- | pretyping/typing.ml | 19 | ||||
| -rw-r--r-- | vernac/himsg.ml | 4 |
7 files changed, 27 insertions, 28 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 diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 36b405e981..816a8c4703 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -28,14 +28,14 @@ open Context.Rel.Declaration let type_of_inductive env (ind,u) = let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in - Typeops.check_hyps_inclusion env mkInd ind mib.mind_hyps; + Typeops.check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps; Inductive.type_of_inductive env (specif,u) (* Return type as quoted by the user *) let type_of_constructor env (cstr,u) = let (mib,_ as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) in - Typeops.check_hyps_inclusion env mkConstruct cstr mib.mind_hyps; + Typeops.check_hyps_inclusion env (GlobRef.ConstructRef cstr) mib.mind_hyps; Inductive.type_of_constructor (cstr,u) specif (* Return constructor types in user form *) diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 4582844b71..b4c19775a7 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -27,6 +27,8 @@ open Arguments_renaming open Pretype_errors open Context.Rel.Declaration +module GR = Names.GlobRef + let meta_type evd mv = let ty = try Evd.meta_ftype evd mv @@ -287,37 +289,36 @@ let judge_of_letin env name defj typj j = { uj_val = mkLetIn (make_annot name r, defj.uj_val, typj.utj_val, j.uj_val) ; uj_type = subst1 defj.uj_val j.uj_type } -let check_hyps_inclusion env sigma f x hyps = +let check_hyps_inclusion env sigma x hyps = let evars = Evarutil.safe_evar_value sigma, Evd.universes sigma in - let f x = EConstr.Unsafe.to_constr (f x) in - Typeops.check_hyps_inclusion env ~evars f x hyps + Typeops.check_hyps_inclusion env ~evars x hyps let type_of_constant env sigma (c,u) = let open Declarations in let cb = Environ.lookup_constant c env in - let () = check_hyps_inclusion env sigma mkConstU (c,u) cb.const_hyps in + let () = check_hyps_inclusion env sigma (GR.ConstRef c) cb.const_hyps in let u = EInstance.kind sigma u in let ty, csts = Environ.constant_type env (c,u) in let sigma = Evd.add_constraints sigma csts in - sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstRef c))) + sigma, (EConstr.of_constr (rename_type ty (GR.ConstRef c))) let type_of_inductive env sigma (ind,u) = let open Declarations in let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in - let () = check_hyps_inclusion env sigma mkIndU (ind,u) mib.mind_hyps in + let () = check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in let u = EInstance.kind sigma u in let ty, csts = Inductive.constrained_type_of_inductive env (specif,u) in let sigma = Evd.add_constraints sigma csts in - sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.IndRef ind))) + sigma, (EConstr.of_constr (rename_type ty (GR.IndRef ind))) let type_of_constructor env sigma ((ind,_ as ctor),u) = let open Declarations in let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in - let () = check_hyps_inclusion env sigma mkIndU (ind,u) mib.mind_hyps in + let () = check_hyps_inclusion env sigma (GR.IndRef ind) mib.mind_hyps in let u = EInstance.kind sigma u in let ty, csts = Inductive.constrained_type_of_constructor (ctor,u) specif in let sigma = Evd.add_constraints sigma csts in - sigma, (EConstr.of_constr (rename_type ty (Names.GlobRef.ConstructRef ctor))) + sigma, (EConstr.of_constr (rename_type ty (GR.ConstructRef ctor))) let judge_of_int env v = Environ.on_judgment EConstr.of_constr (judge_of_int env v) diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 17c3e0395a..dfc4631572 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -201,9 +201,7 @@ let explain_bad_assumption env sigma j = str "because this term is not a type." let explain_reference_variables sigma id c = - (* c is intended to be a global reference *) - let pc = pr_global (fst (Termops.global_of_constr sigma c)) in - pc ++ strbrk " depends on the variable " ++ Id.print id ++ + pr_global c ++ strbrk " depends on the variable " ++ Id.print id ++ strbrk " which is not declared in the context." let rec pr_disjunction pr = function |