diff options
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 8 | ||||
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 18 |
2 files changed, 13 insertions, 13 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 5e128bc423..f2f978ccdf 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -57,7 +57,7 @@ let intern_hyp iconstr globs = function Hprop (intern_statement iconstr globs st) let intern_hyps iconstr globs hyps = - snd (list_fold_map (intern_hyp iconstr) globs hyps) + snd (List.fold_map (intern_hyp iconstr) globs hyps) let intern_cut intern_it globs cut= let nglobs,nstat=intern_it globs cut.cut_stat in @@ -74,10 +74,10 @@ let intern_hyp_list args globs = let intern_one globs (loc,(id,opttyp)) = (add_var id globs), (loc,(id,Option.map (intern_constr globs) opttyp)) in - list_fold_map intern_one globs args + List.fold_map intern_one globs args let intern_suffices_clause globs (hyps,c) = - let nglobs,nhyps = list_fold_map (intern_hyp intern_constr) globs hyps in + let nglobs,nhyps = List.fold_map (intern_hyp intern_constr) globs hyps in nglobs,(nhyps,intern_constr_or_thesis nglobs c) let intern_fundecl args body globs= @@ -340,7 +340,7 @@ let interp_cases info sigma env params (pat:cases_pattern_expr) hyps = (fun (loc,(id,_)) -> GVar (loc,id)) params in let dum_args= - list_tabulate + List.tabulate (fun _ -> GHole (Loc.ghost,Evar_kinds.QuestionMark (Evar_kinds.Define false))) oib.Declarations.mind_nrealargs in glob_app(Loc.ghost,rind,rparams@rparams_rec@dum_args) in diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 31e15081b2..1a0d05047e 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 |