aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/omega
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/omega')
-rw-r--r--plugins/omega/coq_omega.ml12
1 files changed, 4 insertions, 8 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 92b092ffe..334baec8d 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -71,8 +71,7 @@ open Goptions
let _ =
declare_bool_option
- { optsync = false;
- optdepr = false;
+ { optdepr = false;
optname = "Omega system time displaying flag";
optkey = ["Omega";"System"];
optread = read display_system_flag;
@@ -80,8 +79,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = false;
- optdepr = false;
+ { optdepr = false;
optname = "Omega action display flag";
optkey = ["Omega";"Action"];
optread = read display_action_flag;
@@ -89,8 +87,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = false;
- optdepr = false;
+ { optdepr = false;
optname = "Omega old style flag";
optkey = ["Omega";"OldStyle"];
optread = read old_style_flag;
@@ -98,8 +95,7 @@ let _ =
let _ =
declare_bool_option
- { optsync = true;
- optdepr = true;
+ { optdepr = true;
optname = "Omega automatic reset of generated names";
optkey = ["Stable";"Omega"];
optread = read reset_flag;