From 6fcd224c128ae5e81f4cce9d5de1ac45883cfebf Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 12 Sep 2000 11:02:30 +0000
Subject: Modification mkAppL; abstraction via kind_of_term; changement dans
 Reduction

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@597 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/class.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/class.ml')

diff --git a/pretyping/class.ml b/pretyping/class.ml
index 6c0da8c204..ee759ad96d 100644
--- a/pretyping/class.ml
+++ b/pretyping/class.ml
@@ -127,7 +127,7 @@ let constructor_at_head1 t =
       | IsVar id -> t',[],[],CL_Var id,0
       | IsCast (c,_) -> aux c
       | IsAppL(f,args) -> 
-	  let t',_,l,c,_ = aux f in t',args,l,c,List.length args
+	  let t',_,l,c,_ = aux f in t',Array.to_list args,l,c,Array.length args
       | IsProd (_,_,_) -> t',[],[],CL_FUN,0
       | IsLetIn (_,_,_,c) -> aux c
       | IsSort _ -> t',[],[],CL_SORT,0
-- 
cgit v1.2.3