diff options
Diffstat (limited to 'checker')
-rw-r--r-- | checker/indtypes.ml | 12 | ||||
-rw-r--r-- | checker/inductive.ml | 10 | ||||
-rw-r--r-- | checker/modops.ml | 22 | ||||
-rw-r--r-- | checker/subtyping.ml | 4 |
4 files changed, 24 insertions, 24 deletions
diff --git a/checker/indtypes.ml b/checker/indtypes.ml index bcb71fe55..8f11e01c3 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -221,7 +221,7 @@ let allowed_sorts issmall isunit s = -let compute_elim_sorts env_ar params mib arity lc = +let compute_elim_sorts env_ar params arity lc = let inst = extended_rel_list 0 params in let env_params = push_rel_context params env_ar in let lc = Array.map @@ -239,7 +239,7 @@ let compute_elim_sorts env_ar params mib arity lc = allowed_sorts small unit s -let typecheck_one_inductive env params mib mip = +let typecheck_one_inductive env params mip = (* mind_typename and mind_consnames not checked *) (* mind_reloc_tbl, mind_nb_constant, mind_nb_args not checked (VM) *) (* mind_arity_ctxt, mind_arity, mind_nrealargs DONE (typecheck_arity) *) @@ -256,7 +256,7 @@ let typecheck_one_inductive env params mib mip = Array.iter2 check_cons_args mip.mind_nf_lc mip.mind_consnrealdecls; (* mind_kelim: checked by positivity criterion ? *) let sorts = - compute_elim_sorts env params mib mip.mind_arity mip.mind_nf_lc in + compute_elim_sorts env params mip.mind_arity mip.mind_nf_lc in let reject_sort s = not (List.mem_f family_equal s sorts) in if List.exists reject_sort mip.mind_kelim then failwith "elimination not allowed"; @@ -355,7 +355,7 @@ let lambda_implicit_lift n a = (* This removes global parameters of the inductive types in lc (for nested inductive types only ) *) -let abstract_mind_lc env ntyps npars lc = +let abstract_mind_lc ntyps npars lc = if npars = 0 then lc else @@ -448,7 +448,7 @@ let check_positivity_one (env, _,ntypes,_ as ienv) hyps nrecp (_,i as ind) indlc let auxntyp = mib.mind_ntypes in if auxntyp <> 1 then raise (IllFormedInd (LocalNonPos n)); (* The nested inductive type with parameters removed *) - let auxlcvect = abstract_mind_lc env auxntyp auxnpar mip.mind_nf_lc in + let auxlcvect = abstract_mind_lc auxntyp auxnpar mip.mind_nf_lc in (* Extends the environment with a variable corresponding to the inductive def *) let (env',_,_,_ as ienv') = ienv_push_inductive ienv ((mi,u),lpar) in @@ -625,7 +625,7 @@ let check_inductive env kn mib = (* - check arities *) let env_ar = typecheck_arity env0 params mib.mind_packets in (* - check constructor types *) - Array.iter (typecheck_one_inductive env_ar params mib) mib.mind_packets; + Array.iter (typecheck_one_inductive env_ar params) mib.mind_packets; (* check the inferred subtyping relation *) let () = match mib.mind_universes with diff --git a/checker/inductive.ml b/checker/inductive.ml index b1edec556..d15380643 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -797,7 +797,7 @@ let rec subterm_specif renv stack t = | Lambda (x,a,b) -> assert (l=[]); - let spec,stack' = extract_stack renv a stack in + let spec,stack' = extract_stack stack in subterm_specif (push_var renv (x,a,spec)) stack' b (* Metas and evars are considered OK *) @@ -813,7 +813,7 @@ and stack_element_specif = function |SClosure (h_renv,h) -> lazy_subterm_specif h_renv [] h |SArg x -> x -and extract_stack renv a = function +and extract_stack = function | [] -> Lazy.from_val Not_subterm , [] | h::t -> stack_element_specif h, t @@ -845,7 +845,7 @@ let error_illegal_rec_call renv fx (arg_renv,arg) = let error_partial_apply renv fx = raise (FixGuardError (renv.env,NotEnoughArgumentsForFixCall fx)) -let filter_stack_domain env ci p stack = +let filter_stack_domain env p stack = let absctx, ar = dest_lam_assum env p in (* Optimization: if the predicate is not dependent, no restriction is needed and we avoid building the recargs tree. *) @@ -925,7 +925,7 @@ let check_one_fix renv recpos trees def = let case_spec = branches_specif renv (lazy_subterm_specif renv [] c_0) ci in let stack' = push_stack_closures renv l stack in - let stack' = filter_stack_domain renv.env ci p stack' in + let stack' = filter_stack_domain renv.env p stack' in Array.iteri (fun k br' -> let stack_br = push_stack_args case_spec.(k) stack' in check_rec_call renv stack_br br') lrest @@ -968,7 +968,7 @@ let check_one_fix renv recpos trees def = | Lambda (x,a,b) -> assert (l = []); check_rec_call renv [] a ; - let spec, stack' = extract_stack renv a stack in + let spec, stack' = extract_stack stack in check_rec_call (push_var renv (x,a,spec)) stack' b | Prod (x,a,b) -> diff --git a/checker/modops.ml b/checker/modops.ml index c7ad0977a..b92d7bbf1 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -80,7 +80,7 @@ and add_module mb env = let add_module_type mp mtb env = add_module (module_body_of_type mp mtb) env -let strengthen_const mp_from l cb resolver = +let strengthen_const mp_from l cb = match cb.const_body with | Def _ -> cb | _ -> @@ -104,34 +104,34 @@ and strengthen_body : 'a. (_ -> 'a) -> _ -> _ -> 'a generic_module_body -> 'a ge match mb.mod_type with | MoreFunctor _ -> mb | NoFunctor sign -> - let resolve_out,sign_out = strengthen_sig mp_from sign mp_to mb.mod_delta + let resolve_out,sign_out = strengthen_sig mp_from sign mp_to in { mb with mod_expr = mk_expr mp_to; mod_type = NoFunctor sign_out; mod_delta = resolve_out } -and strengthen_sig mp_from sign mp_to resolver = +and strengthen_sig mp_from sign mp_to = match sign with | [] -> empty_delta_resolver,[] | (l,SFBconst cb) :: rest -> - let item' = l,SFBconst (strengthen_const mp_from l cb resolver) in - let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in + let item' = l,SFBconst (strengthen_const mp_from l cb) in + let resolve_out,rest' = strengthen_sig mp_from rest mp_to in resolve_out,item'::rest' | (_,SFBmind _ as item):: rest -> - let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in + let resolve_out,rest' = strengthen_sig mp_from rest mp_to in resolve_out,item::rest' | (l,SFBmodule mb) :: rest -> let mp_from' = MPdot (mp_from,l) in let mp_to' = MPdot(mp_to,l) in let mb_out = strengthen_mod mp_from' mp_to' mb in let item' = l,SFBmodule (mb_out) in - let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in + let resolve_out,rest' = strengthen_sig mp_from rest mp_to in resolve_out (*add_delta_resolver resolve_out mb.mod_delta*), - item':: rest' - | (l,SFBmodtype mty as item) :: rest -> - let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in - resolve_out,item::rest' + item':: rest' + | (_,SFBmodtype _ as item) :: rest -> + let resolve_out,rest' = strengthen_sig mp_from rest mp_to in + resolve_out,item::rest' let strengthen mtb mp = strengthen_body ignore mtb.mod_mp mp mtb diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 6d0d6f6c6..3f7f84470 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -217,7 +217,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= let _ = Array.map2_i check_cons_types mib1.mind_packets mib2.mind_packets in () -let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = +let check_constant env l info1 cb2 spec2 subst1 subst2 = let error () = error_not_match l spec2 in let check_conv f = check_conv_error error f in let check_type env t1 t2 = check_conv conv_leq env t1 t2 in @@ -281,7 +281,7 @@ and check_signatures env mp1 sig1 sig2 subst1 subst2 = let check_one_body (l,spec2) = match spec2 with | SFBconst cb2 -> - check_constant env mp1 l (get_obj mp1 map1 l) + check_constant env l (get_obj mp1 map1 l) cb2 spec2 subst1 subst2 | SFBmind mib2 -> check_inductive env mp1 l (get_obj mp1 map1 l) |