aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/g_ground.ml46
1 files changed, 2 insertions, 4 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index b25017535..bbe1476bc 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -30,8 +30,7 @@ let ground_depth=ref 3
let _=
let gdopt=
- { optsync=true;
- optdepr=false;
+ { optdepr=false;
optname="Firstorder Depth";
optkey=["Firstorder";"Depth"];
optread=(fun ()->Some !ground_depth);
@@ -46,8 +45,7 @@ let congruence_depth=ref 100
let _=
let gdopt=
- { optsync=true;
- optdepr=false;
+ { optdepr=false;
optname="Congruence Depth";
optkey=["Congruence";"Depth"];
optread=(fun ()->Some !congruence_depth);