aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/omega/coq_omega.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/omega/coq_omega.ml')
-rw-r--r--plugins/omega/coq_omega.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 535459885..8c8640ea5 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -61,7 +61,7 @@ let _ =
declare_bool_option
{ optsync = false;
optname = "Omega system time displaying flag";
- optkey = SecondaryTable ("Omega","System");
+ optkey = ["Omega";"System"];
optread = read display_system_flag;
optwrite = write display_system_flag }
@@ -69,7 +69,7 @@ let _ =
declare_bool_option
{ optsync = false;
optname = "Omega action display flag";
- optkey = SecondaryTable ("Omega","Action");
+ optkey = ["Omega";"Action"];
optread = read display_action_flag;
optwrite = write display_action_flag }
@@ -77,7 +77,7 @@ let _ =
declare_bool_option
{ optsync = false;
optname = "Omega old style flag";
- optkey = SecondaryTable ("Omega","OldStyle");
+ optkey = ["Omega";"OldStyle"];
optread = read old_style_flag;
optwrite = write old_style_flag }