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, 2 insertions, 0 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index a78532e33..cec3505a9 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -153,6 +153,8 @@ TACTIC EXTEND gintuition
END
open Proofview.Notations
+open Cc_plugin
+open Decl_mode_plugin
let default_declarative_automation =
Proofview.tclUNIT () >>= fun () -> (* delay for [congruence_depth] *)