From 8568214f1b7950fe9c5d95c04e851c00f49751ce Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 16 Apr 2003 22:23:58 +0000
Subject: 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
---
 pretyping/cbv.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/cbv.ml')

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 *)
-- 
cgit v1.2.3