aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--contrib/first-order/g_ground.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4
index bfdf5dbfc1..2c2fd13032 100644
--- a/contrib/first-order/g_ground.ml4
+++ b/contrib/first-order/g_ground.ml4
@@ -95,9 +95,9 @@ TACTIC EXTEND GTauto
[ "GTauto" ] ->
[ gen_ground_tac false (Some fail_solver) Void ]
END
+*)
TACTIC EXTEND GIntuition
[ "GIntuition" tactic_opt(t) ] ->
[ gen_ground_tac false (option_app eval_tactic t) Void ]
END
-*)