aboutsummaryrefslogtreecommitdiff
path: root/plugins/rtauto/proof_search.ml
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/rtauto/proof_search.ml
parent99d129b8e4e7fcde8c848520463c4e8c7d8bdc11 (diff)
s/let _ =/let () =/ in some places (mostly goptions related)
Diffstat (limited to 'plugins/rtauto/proof_search.ml')
-rw-r--r--plugins/rtauto/proof_search.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 3de5923968..aab1e47555 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -54,7 +54,7 @@ let opt_pruning=
optread=(fun () -> !pruning);
optwrite=(fun b -> pruning:=b)}
-let _ = declare_bool_option opt_pruning
+let () = declare_bool_option opt_pruning
type form=
Atom of int