aboutsummaryrefslogtreecommitdiff
path: root/plugins/firstorder
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-11-21 20:00:46 +0100
committerGaëtan Gilbert2018-11-23 13:21:31 +0100
commit74038abdd41161a4c4b1eba5dbbd83f5c0301bf3 (patch)
treef1932098c3b1320ebf8629c2b22f9437608e6fcf /plugins/firstorder
parent99d129b8e4e7fcde8c848520463c4e8c7d8bdc11 (diff)
s/let _ =/let () =/ in some places (mostly goptions related)
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 *)