From e138fbf1e1cd95bfae05e17074f94a1ebde2edf8 Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Sat, 18 Jan 2020 20:35:42 +0100
Subject: firstorder: default tactic is “auto with core”

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

(limited to 'plugins')

diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index 0133a02ca7..49e4c91182 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -47,7 +47,7 @@ let ()=
 
 
 let default_intuition_tac =
-  let tac _ _ = Auto.h_auto None [] None in
+  let tac _ _ = Auto.h_auto None [] (Some []) in
   let name = { Tacexpr.mltac_plugin = "ground_plugin"; mltac_tactic = "auto_with"; } in
   let entry = { Tacexpr.mltac_name = name; mltac_index = 0 } in
   Tacenv.register_ml_tactic name [| tac |];
-- 
cgit v1.2.3