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 /tactics/termdn.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 'tactics/termdn.ml')
| -rw-r--r-- | tactics/termdn.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/termdn.ml b/tactics/termdn.ml index 920e6ba310..c62746cc71 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -17,7 +17,7 @@ type 'a t = (constr_label,constr_pattern,'a) Dn.t let decomp = let rec decrec acc c = match kind_of_term c with - | IsAppL (f,l) -> decrec (l@acc) f + | IsAppL (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f | IsCast (c1,_) -> decrec acc c1 | _ -> (c,acc) in |