diff options
| -rw-r--r-- | Makefile | 4 | ||||
| -rw-r--r-- | kernel/instantiate.ml | 35 | ||||
| -rw-r--r-- | kernel/instantiate.mli | 9 |
3 files changed, 4 insertions, 44 deletions
@@ -65,9 +65,9 @@ LIB=lib/pp_control.cmo lib/pp.cmo lib/util.cmo \ KERNEL=kernel/names.cmo kernel/generic.cmo kernel/univ.cmo kernel/term.cmo \ kernel/sign.cmo kernel/constant.cmo \ - kernel/inductive.cmo kernel/sosub.cmo kernel/abstraction.cmo \ + kernel/sosub.cmo kernel/abstraction.cmo \ kernel/environ.cmo kernel/evd.cmo kernel/instantiate.cmo \ - kernel/closure.cmo kernel/reduction.cmo \ + kernel/closure.cmo kernel/reduction.cmo kernel/inductive.cmo\ kernel/type_errors.cmo kernel/typeops.cmo kernel/indtypes.cmo \ kernel/safe_typing.cmo diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml index 5e48b8e0c2..37e2c310c4 100644 --- a/kernel/instantiate.ml +++ b/kernel/instantiate.ml @@ -9,7 +9,6 @@ open Term open Sign open Evd open Constant -open Inductive open Environ let is_id_inst ids args = @@ -55,28 +54,6 @@ let constant_value env cst = anomalylabstrm "termenv__constant_value" [< 'sTR "a defined constant with no body." >] -let mis_lc mis = - instantiate_constr (ids_of_sign mis.mis_mib.mind_hyps) mis.mis_mip.mind_lc - (Array.to_list mis.mis_args) - -let mis_lc_without_abstractions mis = - let rec strip_DLAM = function - | (DLAM (n,c1)) -> strip_DLAM c1 - | (DLAMV (n,v)) -> v - | _ -> assert false - in - strip_DLAM (mis_lc mis) - -let mis_type_mconstructs mispec = - let specif = mis_lc mispec - and ntypes = mis_ntypes mispec - and nconstr = mis_nconstr mispec in - let make_Ik k = DOPN(MutInd(mispec.mis_sp,k),mispec.mis_args) - and make_Ck k = DOPN(MutConstruct((mispec.mis_sp,mispec.mis_tyi),k+1), - mispec.mis_args) in - (Array.init nconstr make_Ck, - sAPPVList specif (list_tabulate make_Ik ntypes)) - (* Existentials. *) let name_of_existential n = id_of_string ("?" ^ string_of_int n) @@ -85,8 +62,8 @@ let existential_type sigma c = let (n,args) = destEvar c in let info = Evd.map sigma n in let hyps = evar_hyps info in - instantiate_constr (ids_of_sign hyps) info.evar_concl - (Array.to_list args) + (* TODO: check args [this comment was in Typeops] *) + instantiate_constr (ids_of_sign hyps) info.evar_concl (Array.to_list args) let existential_value sigma c = let (n,args) = destEvar c in @@ -111,11 +88,3 @@ let const_abst_opt_value env sigma c = if evaluable_abst env c then Some (abst_value env c) else None | _ -> invalid_arg "const_abst_opt_value" -let mis_typed_arity mis = - let idhyps = ids_of_sign mis.mis_mib.mind_hyps - and largs = Array.to_list mis.mis_args in - instantiate_type idhyps mis.mis_mip.mind_arity largs - -let mis_arity mispec = incast_type (mis_typed_arity mispec) - - diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli index 8d267021f5..302927074e 100644 --- a/kernel/instantiate.mli +++ b/kernel/instantiate.mli @@ -28,12 +28,3 @@ val existential_value : 'a evar_map -> constr -> constr val existential_type : 'a evar_map -> constr -> constr val const_abst_opt_value : env -> 'a evar_map -> constr -> constr option - -val mis_typed_arity : mind_specif -> typed_type -val mis_arity : mind_specif -> constr - -val mis_lc : mind_specif -> constr -val mis_lc_without_abstractions : mind_specif -> constr array - -val mis_type_mconstructs : mind_specif -> constr array * constr array - |