simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = list_skipn n l

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3931 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 9 insertions, 9 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a0deab683c..bd38d5c867 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 d1d9206fab..2599e2958f 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 1b7a515b93..161c37ae80 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 60700d295b..2da3748d5d 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 a2e484f532..b2d60176da 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 2a74ede726..7dc78cbe61 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 =