aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/g_ground.mlg4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index a212d13453..37fc81ee38 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -33,7 +33,7 @@ DECLARE PLUGIN "ground_plugin"
let ground_depth=ref 3
-let _=
+let ()=
let gdopt=
{ optdepr=false;
optname="Firstorder Depth";
@@ -47,7 +47,7 @@ let _=
declare_int_option gdopt
-let _=
+let ()=
let congruence_depth=ref 100 in
let gdopt=
{ optdepr=true; (* noop *)