aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/tactics.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d8c2411934..7ee45523f5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3470,8 +3470,8 @@ let ids_of_constr ?(all=false) vars c =
Array.fold_left_from
(if all then 0 else mib.Declarations.mind_nparams)
aux vars args
- | _ -> fold_constr aux vars c)
- | _ -> fold_constr aux vars c
+ | _ -> Term.fold_constr aux vars c)
+ | _ -> Term.fold_constr aux vars c
in aux vars c
let decompose_indapp f args =