diff options
Diffstat (limited to 'plugins/firstorder/g_ground.ml4')
| -rw-r--r-- | plugins/firstorder/g_ground.ml4 | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index c1b7b63c3..4a38c48dc 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -27,6 +27,7 @@ let ground_depth=ref 3 let _= let gdopt= { optsync=true; + optdepr=false; optname="Firstorder Depth"; optkey=["Firstorder";"Depth"]; optread=(fun ()->Some !ground_depth); @@ -42,6 +43,7 @@ let congruence_depth=ref 100 let _= let gdopt= { optsync=true; + optdepr=false; optname="Congruence Depth"; optkey=["Congruence";"Depth"]; optread=(fun ()->Some !congruence_depth); |