aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/class_tactics.ml
diff options
context:
space:
mode:
authorGravatar Matej Kosik <m4tej.kosik@gmail.com>2016-08-30 10:47:37 +0200
committerGravatar Matej Kosik <m4tej.kosik@gmail.com>2016-08-30 10:47:37 +0200
commit2ff6d31c7a6011b26dfa7f0b2bb593b356833058 (patch)
tree82a3b37c697a2f4b2512cca8ebd72135dfb9673d /tactics/class_tactics.ml
parent24f70f4173726c5c4734a6f8f907d4bf4a0124ea (diff)
CLEANUP: using |> operator more consistently
Diffstat (limited to 'tactics/class_tactics.ml')
-rw-r--r--tactics/class_tactics.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 8c43ac8b5..1672b7bd1 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -565,7 +565,7 @@ let make_hints g st only_classes sign =
List.fold_left
(fun hints hyp ->
let consider =
- try let t = Global.lookup_named (NamedDecl.get_id hyp) |> NamedDecl.get_type in
+ try let t = hyp |> NamedDecl.get_id |> Global.lookup_named |> NamedDecl.get_type in
(* Section variable, reindex only if the type changed *)
not (Term.eq_constr t (NamedDecl.get_type hyp))
with Not_found -> true