aboutsummaryrefslogtreecommitdiff
path: root/plugins/rtauto/proof_search.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/rtauto/proof_search.ml')
-rw-r--r--plugins/rtauto/proof_search.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 4cc32cfb26..ab34489de9 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -49,7 +49,6 @@ let pruning = ref true
let opt_pruning=
{optdepr=false;
- optname="Rtauto Pruning";
optkey=["Rtauto";"Pruning"];
optread=(fun () -> !pruning);
optwrite=(fun b -> pruning:=b)}