aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
authorMatej Kosik2016-08-14 18:36:30 +0200
committerMatej Kosik2016-08-25 07:53:02 +0200
commit4688a3b9750827eb0f5f61066ca617efcd97bc8c (patch)
tree33289dff2847f51ef99f7711bee7624ca80a9341 /tactics
parent16ecabd99d66b3068e17fae486ba4ed77954e813 (diff)
CLEANUP: functions "Context.{Rel,Named}.Context.fold" were renamed to "Context.{Rel,Named}.fold_constr"
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 =