aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder/g_ground.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder/g_ground.ml4')
-rw-r--r--plugins/firstorder/g_ground.ml42
1 files changed, 1 insertions, 1 deletions
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 []))