diff options
author | 2016-08-30 10:47:37 +0200 | |
---|---|---|
committer | 2016-08-30 10:47:37 +0200 | |
commit | 2ff6d31c7a6011b26dfa7f0b2bb593b356833058 (patch) | |
tree | 82a3b37c697a2f4b2512cca8ebd72135dfb9673d /tactics/class_tactics.ml | |
parent | 24f70f4173726c5c4734a6f8f907d4bf4a0124ea (diff) |
CLEANUP: using |> operator more consistently
Diffstat (limited to 'tactics/class_tactics.ml')
-rw-r--r-- | tactics/class_tactics.ml | 2 |
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 |