From 27d780bd52e1776afb05793d43ac030af861c82d Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack <arnaud@spiwack.net>
Date: Thu, 27 Feb 2014 12:54:29 +0100
Subject: Proofview.Notations: Now that (>>=) is free, use it for tclBIND.

Impacts MapleMode.
---
 plugins/firstorder/g_ground.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/firstorder/g_ground.ml4')

diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index c125be65a..563148872 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -141,7 +141,7 @@ END
 open Proofview.Notations
 
 let default_declarative_automation =
-  Proofview.tclUNIT () >= fun () -> (* delay for [congruence_depth] *)
+  Proofview.tclUNIT () >>= fun () -> (* delay for [congruence_depth] *)
   Tacticals.New.tclORELSE
     (Tacticals.New.tclORELSE (Auto.h_trivial [] None)
     (Cctac.congruence_tac !congruence_depth []))
-- 
cgit v1.2.3