diff options
Diffstat (limited to 'plugins/firstorder/g_ground.ml4')
| -rw-r--r-- | plugins/firstorder/g_ground.ml4 | 6 |
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); |