diff options
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 32 |
1 files changed, 15 insertions, 17 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index c74bfd0688..19d76bfee6 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -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,19 +368,19 @@ 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 + (spec,u) (Inductive.make_param_univs env 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; - let t,cst = Inductive.constrained_type_of_inductive env ((mib,mip),u) in + check_hyps_inclusion env (GlobRef.IndRef ind) mib.mind_hyps; + let t,cst = Inductive.constrained_type_of_inductive ((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 @@ -461,8 +461,7 @@ let type_of_global_in_context env r = let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in let univs = Declareops.inductive_polymorphic_context mib in let inst = Univ.make_abstract_instance univs in - let env = Environ.push_context ~strict:false (Univ.AUContext.repr univs) env in - Inductive.type_of_inductive env (specif, inst), univs + Inductive.type_of_inductive (specif, inst), univs | ConstructRef cstr -> let (mib,_ as specif) = Inductive.lookup_mind_specif env (inductive_of_constructor cstr) @@ -515,8 +514,7 @@ let rec execute env cstr = let f', ft = match kind f with | Ind ind when Environ.template_polymorphic_pind ind env -> - let args = Array.map (fun t -> lazy t) argst in - f, type_of_inductive_knowing_parameters env ind args + f, type_of_inductive_knowing_parameters env ind argst | _ -> (* No template polymorphism *) execute env f |