diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2016-08-30 10:47:37 +0200 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-08-30 10:47:37 +0200 |
| commit | 2ff6d31c7a6011b26dfa7f0b2bb593b356833058 (patch) | |
| tree | 82a3b37c697a2f4b2512cca8ebd72135dfb9673d /tactics | |
| parent | 24f70f4173726c5c4734a6f8f907d4bf4a0124ea (diff) | |
CLEANUP: using |> operator more consistently
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/class_tactics.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 |
2 files changed, 3 insertions, 3 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 diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 7ee45523f..51bbd9058 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2783,7 +2783,7 @@ let old_generalize_dep ?(with_let=false) c gl = let body = if with_let then match kind_of_term c with - | Var id -> Tacmach.pf_get_hyp gl id |> NamedDecl.get_value + | Var id -> id |> Tacmach.pf_get_hyp gl |> NamedDecl.get_value | _ -> None else None in @@ -3561,7 +3561,7 @@ let linear vars args = with Seen -> false let is_defined_variable env id = - lookup_named id env |> is_local_def + env |> lookup_named id |> is_local_def let abstract_args gl generalize_vars dep id defined f args = let open Context.Rel.Declaration in |