diff options
Diffstat (limited to 'plugins/firstorder')
| -rw-r--r-- | plugins/firstorder/g_ground.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index d7c5b66ae7..96c5bcae4f 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -30,7 +30,7 @@ let _= let gdopt= { optsync=true; optname="Firstorder Depth"; - optkey=SecondaryTable("Firstorder","Depth"); + optkey=["Firstorder";"Depth"]; optread=(fun ()->Some !ground_depth); optwrite= (function @@ -45,7 +45,7 @@ let _= let gdopt= { optsync=true; optname="Congruence Depth"; - optkey=SecondaryTable("Congruence","Depth"); + optkey=["Congruence";"Depth"]; optread=(fun ()->Some !congruence_depth); optwrite= (function |