aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrextern.ml2
-rw-r--r--kernel/closure.ml6
-rw-r--r--kernel/inductive.ml2
-rw-r--r--library/libnames.ml5
-rw-r--r--parsing/egrammar.ml2
-rw-r--r--parsing/termast.ml2
-rw-r--r--pretyping/cases.ml2
-rw-r--r--pretyping/cbv.ml2
-rw-r--r--pretyping/indrec.ml4
-rw-r--r--pretyping/inductiveops.ml4
-rw-r--r--pretyping/reductionops.ml2
-rw-r--r--pretyping/tacred.ml4
-rw-r--r--tactics/eqdecide.ml42
13 files changed, 18 insertions, 21 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index d07934f7d..75f8e7abc 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -182,7 +182,7 @@ let rec skip_coercion dest_ref (f,args as app) =
| Some n ->
if n >= List.length args then app
else (* We skip a coercion *)
- let _,fargs = list_chop n args in
+ let fargs = list_skipn n args in
skip_coercion dest_ref (List.hd fargs,List.tl fargs)
| None -> app)
| None -> app
diff --git a/kernel/closure.ml b/kernel/closure.ml
index c3b828a39..1e7dadb04 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -474,9 +474,7 @@ let rec stack_tail p s =
| Zapp args :: s ->
let q = List.length args in
if p >= q then stack_tail (p-q) s
- else
- let (_,aft) = list_chop p args in
- Zapp aft :: s
+ else Zapp (list_skipn p args) :: s
| _ -> failwith "stack_tail"
let rec stack_nth s p = match s with
| Zapp args :: s ->
@@ -823,7 +821,7 @@ let rec drop_parameters depth n stk =
if n > q then drop_parameters depth (n-q) s
else if n = q then reloc_rargs depth s
else
- let (_,aft) = list_chop n args in
+ let aft = list_skipn n args in
reloc_rargs depth (append_stack_list (aft,s))
| Zshift(k)::s -> drop_parameters (depth-k) n s
| [] -> assert (n=0); []
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index e8795982f..13dd9c550 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -763,7 +763,7 @@ let check_one_cofix env nbfix def deftype =
let lra =vlra.(i-1) in
let mI = inductive_of_constructor cstr_kn in
let (mib,mip) = lookup_mind_specif env mI in
- let _,realargs = list_chop mip.mind_nparams args in
+ let realargs = list_skipn mip.mind_nparams args in
let rec process_args_of_constr = function
| (t::lr), (rar::lrar) ->
if rar = mk_norec then
diff --git a/library/libnames.ml b/library/libnames.ml
index 00a28b71f..9a8439804 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -62,8 +62,7 @@ let pr_dirpath sl = (str (string_of_dirpath sl))
(* Pop the last n module idents *)
let extract_dirpath_prefix n dir =
- let (_,dir') = list_chop n (repr_dirpath dir) in
- make_dirpath dir'
+ make_dirpath (list_skipn n (repr_dirpath dir))
let dirpath_prefix p = match repr_dirpath p with
| [] -> anomaly "dirpath_prefix: empty dirpath"
@@ -164,7 +163,7 @@ let pr_sp sp = str (string_of_path sp)
let restrict_path n sp =
let dir, s = repr_path sp in
- let (dir',_) = list_chop n (repr_dirpath dir) in
+ let dir' = list_firstn n (repr_dirpath dir) in
make_path (make_dirpath dir') s
type extended_global_reference =
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 77ac447c9..ef3919c81 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -120,7 +120,7 @@ let find_position other assoc lev =
Some (Gramext.Level (constr_level (n,a))), None, None
let remove_levels n =
- level_stack := snd (list_chop n !level_stack)
+ level_stack := list_skipn n !level_stack
(* Interpretation of the right hand side of grammar rules *)
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 236a35ca7..299c061c9 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -173,7 +173,7 @@ let rec skip_coercion dest_ref (f,args as app) =
| Some n ->
if n >= List.length args then app
else (* We skip a coercion *)
- let _,fargs = list_chop n args in
+ let fargs = list_skipn n args in
skip_coercion dest_ref (List.hd fargs,List.tl fargs)
| None -> app)
| None -> app
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a0deab683..bd38d5c86 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -779,7 +779,7 @@ let push_rels_eqn sign eqn =
{eqn with rhs = {eqn.rhs with rhs_env = push_rels sign eqn.rhs.rhs_env} }
let push_rels_eqn_with_names sign eqn =
- let pats = List.rev (fst (list_chop (List.length sign) eqn.patterns)) in
+ let pats = List.rev (list_firstn (List.length sign) eqn.patterns) in
let sign = recover_alias_names alias_of_pat pats sign in
push_rels_eqn sign eqn
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index d1d9206fa..2599e2958 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -273,7 +273,7 @@ and cbv_stack_term info stack env t =
(* constructor in a Case -> IOTA *)
| (CONSTR((sp,n),_), APP(args,CASE(_,br,ci,env,stk)))
when red_set (info_flags info) fIOTA ->
- let real_args = snd (list_chop ci.ci_npar args) in
+ let real_args = list_skipn ci.ci_npar args in
cbv_stack_term info (stack_app real_args stk) env br.(n-1)
(* constructor of arity 0 in a Case -> IOTA *)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 1b7a515b9..161c37ae8 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -118,7 +118,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
let d = (n,Some b,t) in
mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::sign) c)
| Ind (_,_) ->
- let (_,realargs) = list_chop nparams largs in
+ let realargs = list_skipn nparams largs in
let base = applist (lift i pk,realargs) in
if depK then
Reduction.beta_appvect
@@ -193,7 +193,7 @@ let make_rec_branch_arg env sigma (nparams,fvect,decF) f cstr recargs =
let d = (n,Some b,t) in
mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c)
| Ind _ ->
- let (_,realargs) = list_chop nparams largs
+ let realargs = list_skipn nparams largs
and arg = appvect (mkRel (i+1),extended_rel_vect 0 hyps) in
applist(lift i fk,realargs@[arg])
| _ -> assert false
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 60700d295..2da3748d5 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -139,7 +139,7 @@ let get_constructor (ind,mib,mip,params) j =
let typi = instantiate_params typi params mip.mind_params_ctxt in
let (args,ccl) = decompose_prod_assum typi in
let (_,allargs) = decompose_app ccl in
- let (_,vargs) = list_chop mip.mind_nparams allargs in
+ let vargs = list_skipn mip.mind_nparams allargs in
{ cs_cstr = ith_constructor_of_inductive ind j;
cs_params = params;
cs_nargs = rel_context_length args;
@@ -277,7 +277,7 @@ let type_case_branches_with_names env indspec pj c =
let (ind,args) = indspec in
let (lbrty,conclty,_) = Inductive.type_case_branches env indspec pj c in
let (mib,mip) = Inductive.lookup_mind_specif env ind in
- let params = fst (list_chop mip.mind_nparams args) in
+ let params = list_firstn mip.mind_nparams args in
if is_dependent_elimination env pj.uj_type (ind,params) then
(set_pattern_names env ind lbrty, conclty)
else (lbrty, conclty)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index a2e484f53..b2d60176d 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -190,7 +190,7 @@ let reduce_mind_case mia =
match kind_of_term mia.mconstr with
| Construct (ind_sp,i as cstr_sp) ->
(* let ncargs = (fst mia.mci).(i-1) in*)
- let real_cargs = snd (list_chop mia.mci.ci_npar mia.mcargs) in
+ let real_cargs = list_skipn mia.mci.ci_npar mia.mcargs in
applist (mia.mlf.(i-1),real_cargs)
| CoFix cofix ->
let cofix_def = contract_cofix cofix in
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 2a74ede72..7dc78cbe6 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -299,7 +299,7 @@ let rev_firstn_liftn fn ln =
To check ... *)
let make_elim_fun (names,(nbfix,lv,n)) largs =
- let labs,_ = list_chop n (list_of_stack largs) in
+ let labs = list_firstn n (list_of_stack largs) in
let p = List.length lv in
let ylv = List.map fst lv in
let la' = list_map_i
@@ -370,7 +370,7 @@ let contract_cofix_use_function f (bodynum,(_,names,bodies as typedbodies)) =
let reduce_mind_case_use_function func env mia =
match kind_of_term mia.mconstr with
| Construct(ind_sp,i as cstr_sp) ->
- let real_cargs = snd (list_chop mia.mci.ci_npar mia.mcargs) in
+ let real_cargs = list_skipn mia.mci.ci_npar mia.mcargs in
applist (mia.mlf.(i-1), real_cargs)
| CoFix (_,(names,_,_) as cofix) ->
let build_fix_name i =
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index a14a7b2de..22f0d36af 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -131,7 +131,7 @@ let solveLeftBranch rectype g =
| _ :: lhs :: rhs :: _ ->
let (mib,mip) = Global.lookup_inductive rectype in
let nparams = mip.mind_nparams in
- let getargs l = snd (list_chop nparams (snd (decompose_app l))) in
+ let getargs l = list_skipn nparams (snd (decompose_app l)) in
let rargs = getargs (snd rhs)
and largs = getargs (snd lhs) in
List.fold_right2
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 11:05:51 +0000