aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/btauto
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/btauto')
-rw-r--r--plugins/btauto/refl_btauto.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 4585468ad..440309284 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -217,7 +217,7 @@ module Btauto = struct
Tacticals.tclFAIL 0 msg gl
let try_unification env =
- Proofview.Goal.concl >>- fun concl ->
+ Proofview.Goal.concl >>= fun concl ->
let eq = Lazy.force eq in
let t = decomp_term concl in
match t with
@@ -230,7 +230,7 @@ module Btauto = struct
Tacticals.New.tclFAIL 0 msg
let tac =
- Proofview.Goal.concl >>- fun concl ->
+ Proofview.Goal.concl >>= fun concl ->
let eq = Lazy.force eq in
let bool = Lazy.force Bool.typ in
let t = decomp_term concl in