aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/termdn.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/termdn.ml')
-rw-r--r--tactics/termdn.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 1837b7945..3a1df0234 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -18,7 +18,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 (Array.fold_right (fun a l -> a::l) l acc) f
+ | IsApp (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f
| IsCast (c1,_) -> decrec acc c1
| _ -> (c,acc)
in