Skip to content

Commit 447f7ae

Browse files
committed
fix precedence
1 parent 059ad5b commit 447f7ae

1 file changed

Lines changed: 3 additions & 3 deletions

File tree

src/ecHiGoal.ml

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -758,14 +758,14 @@ let process_rewrite1_r ttenv ?target ri tc =
758758
match simpl with
759759
| Some logic ->
760760
let hyps = FApi.tc1_hyps tc in
761-
let target = target |> omap (fst -| LDecl.hyp_by_name^~ hyps -| unloc) in
761+
let target = target |> omap (fst -| ((LDecl.hyp_by_name^~ hyps) -| unloc)) in
762762
t_simplify_lg ?target ~delta:`IfApplied (ttenv, logic)
763763
| None -> t_id
764764
in FApi.t_seq tt process_trivial tc
765765

766766
| RWSimpl logic ->
767767
let hyps = FApi.tc1_hyps tc in
768-
let target = target |> omap (fst -| LDecl.hyp_by_name^~ hyps -| unloc) in
768+
let target = target |> omap (fst -| ((LDecl.hyp_by_name^~ hyps) -| unloc)) in
769769
t_simplify_lg ?target ~delta:`IfApplied (ttenv, logic) tc
770770

771771
| RWDelta ((s, r, o, px), p) -> begin
@@ -782,7 +782,7 @@ let process_rewrite1_r ttenv ?target ri tc =
782782
| RWRw (((s : rwside), r, o, p), pts) -> begin
783783
let do1 (mode : [`Full | `Light]) ((subs : rwside), pt) tc =
784784
let hyps = FApi.tc1_hyps tc in
785-
let target = target |> omap (fst -| LDecl.hyp_by_name^~ hyps -| unloc) in
785+
let target = target |> omap (fst -| ((LDecl.hyp_by_name^~ hyps) -| unloc)) in
786786
let hyps = FApi.tc1_hyps ?target tc in
787787

788788
let ptenv, prw =

0 commit comments

Comments
 (0)