diff options
| author | herbelin | 2000-09-12 11:02:30 +0000 |
|---|---|---|
| committer | herbelin | 2000-09-12 11:02:30 +0000 |
| commit | 6fcd224c128ae5e81f4cce9d5de1ac45883cfebf (patch) | |
| tree | 9d5c886b18ca44f3a24de7b58c7dd7ca8bc88eec /pretyping/class.ml | |
| parent | 9248485d71d1c9c1796a22e526e07784493e2008 (diff) | |
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
Diffstat (limited to 'pretyping/class.ml')
| -rw-r--r-- | pretyping/class.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 |