diff options
| author | letouzey | 2003-04-16 22:23:58 +0000 |
|---|---|---|
| committer | letouzey | 2003-04-16 22:23:58 +0000 |
| commit | 8568214f1b7950fe9c5d95c04e851c00f49751ce (patch) | |
| tree | 91d2fe6ba491c2e7df9ef28eccffcfe37fd286da /pretyping/inductiveops.ml | |
| parent | 391605f6195f92603ca960014db302dc79e6d24f (diff) | |
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
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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) |