diff options
Diffstat (limited to 'plugins/decl_mode/decl_proof_instr.ml')
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 31e15081b..1a0d05047 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -857,7 +857,7 @@ let build_per_info etype casee gls = match etype with ET_Induction -> mind.mind_nparams_rec,Some (snd ind) | _ -> mind.mind_nparams,None in - let params,real_args = list_chop nparams args in + let params,real_args = List.chop nparams args in let abstract_obj c body = let typ=pf_type_of gls c in lambda_create env (typ,subst_term c body) in @@ -953,7 +953,7 @@ let rec tree_of_pats ((id,_) as cpl) pats = let nexti i ati = if i = pred cnum then let nargs = - list_map_i (fun j a -> (a,ati.(j))) 0 args in + List.map_i (fun j a -> (a,ati.(j))) 0 args in Some (Idset.singleton id, tree_of_pats cpl (nargs::rest_args::stack)) else None @@ -998,7 +998,7 @@ let rec add_branch ((id,_) as cpl) pats tree= let nexti i ati = if i = pred cnum then let nargs = - list_map_i (fun j a -> (a,ati.(j))) 0 args in + List.map_i (fun j a -> (a,ati.(j))) 0 args in Some (Idset.add id ids, add_branch cpl (nargs::rest_args::stack) (skip_args t ids (Array.length ati))) @@ -1013,7 +1013,7 @@ let rec add_branch ((id,_) as cpl) pats tree= let mapi i ati bri = if i = pred cnum then let nargs = - list_map_i (fun j a -> (a,ati.(j))) 0 args in + List.map_i (fun j a -> (a,ati.(j))) 0 args in append_branch cpl 0 (nargs::rest_args::stack) bri else bri in @@ -1051,7 +1051,7 @@ let thesis_for obj typ per_info env= errorlabstrm "thesis_for" ((Printer.pr_constr_env env obj) ++ spc () ++ str"cannot give an induction hypothesis (wrong inductive type).") in - let params,args = list_chop per_info.per_nparams all_args in + let params,args = List.chop per_info.per_nparams all_args in let _ = if not (List.for_all2 eq_constr params per_info.per_params) then errorlabstrm "thesis_for" ((Printer.pr_constr_env env obj) ++ spc () ++ @@ -1182,7 +1182,7 @@ let hrec_for fix_id per_info gls obj_id = let rc,hd1=decompose_prod typ in let cind,all_args=decompose_app typ in let ind = destInd cind in assert (ind=per_info.per_ind); - let params,args= list_chop per_info.per_nparams all_args in + let params,args= List.chop per_info.per_nparams all_args in assert begin try List.for_all2 eq_constr params per_info.per_params with Invalid_argument _ -> false end; @@ -1203,8 +1203,8 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = match List.assoc id args with [None,br_args] -> let all_metas = - list_tabulate (fun n -> mkMeta (succ n)) (nparams + nhyps) in - let param_metas,hyp_metas = list_chop nparams all_metas in + List.tabulate (fun n -> mkMeta (succ n)) (nparams + nhyps) in + let param_metas,hyp_metas = List.chop nparams all_metas in tclTHEN (tclDO nhrec introf) (tacnext @@ -1221,7 +1221,7 @@ let rec execute_cases fix_name per_info tacnext args objs nhrec tree gls = let ctyp=pf_type_of gls casee in let hd,all_args = decompose_app (special_whd gls ctyp) in let _ = assert (destInd hd = ind) in (* just in case *) - let params,real_args = list_chop nparams all_args in + let params,real_args = List.chop nparams all_args in let abstract_obj c body = let typ=pf_type_of gls c in lambda_create env (typ,subst_term c body) in |