1 files changed, 4 insertions, 6 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 33a9dd4fd..6281b2675 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -1,5 +1,3 @@
-open Proofview.Notations
-
 let contrib_name = "btauto"
 
 let init_constant dir s =
@@ -219,7 +217,7 @@ module Btauto = struct
     Tacticals.tclFAIL 0 msg gl
 
   let try_unification env =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.nf_enter begin fun gl ->
       let concl = Proofview.Goal.concl gl in
       let eq = Lazy.force eq in
       let concl = EConstr.Unsafe.to_constr concl in
@@ -232,10 +230,10 @@ module Btauto = struct
       | _ ->
           let msg = str "Btauto: Internal error" in
           Tacticals.New.tclFAIL 0 msg
-    end }
+    end
 
   let tac =
-    Proofview.Goal.nf_enter { enter = begin fun gl ->
+    Proofview.Goal.nf_enter begin fun gl ->
       let concl = Proofview.Goal.concl gl in
       let concl = EConstr.Unsafe.to_constr concl in
       let sigma = Tacmach.New.project gl in
@@ -262,6 +260,6 @@ module Btauto = struct
       | _ ->
           let msg = str "Cannot recognize a boolean equality" in
           Tacticals.New.tclFAIL 0 msg
-    end }
+    end
 
 end