aboutsummaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-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 da1d0dcbdd..ebfb0e0181 100644
--- a/contrib/first-order/g_ground.ml4
+++ b/contrib/first-order/g_ground.ml4
@@ -95,7 +95,7 @@ TACTIC EXTEND Ground
END
TACTIC EXTEND GTauto
- [ "Tauto" ] ->
+ [ "GTauto" ] ->
[ gen_ground_tac false (Some fail_solver) Void ]
END