diff options
Diffstat (limited to 'vernac')
-rw-r--r-- | vernac/classes.ml | 1 | ||||
-rw-r--r-- | vernac/indschemes.ml | 24 | ||||
-rw-r--r-- | vernac/lemmas.ml | 3 | ||||
-rw-r--r-- | vernac/obligations.ml | 6 | ||||
-rw-r--r-- | vernac/record.ml | 9 | ||||
-rw-r--r-- | vernac/search.ml | 1 | ||||
-rw-r--r-- | vernac/vernacentries.ml | 87 |
7 files changed, 43 insertions, 88 deletions
diff --git a/vernac/classes.ml b/vernac/classes.ml index d515b0c9b..e760487bd 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -32,7 +32,6 @@ open Entries let refine_instance = ref true let _ = Goptions.declare_bool_option { - Goptions.optsync = true; Goptions.optdepr = false; Goptions.optname = "definition of instances by refining"; Goptions.optkey = ["Refine";"Instance";"Mode"]; diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 9ba4e46e4..2458c5131 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -45,8 +45,7 @@ open Context.Rel.Declaration let elim_flag = ref true let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "automatic declaration of induction schemes"; optkey = ["Elimination";"Schemes"]; optread = (fun () -> !elim_flag) ; @@ -55,16 +54,14 @@ let _ = let bifinite_elim_flag = ref false let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "automatic declaration of induction schemes for non-recursive types"; optkey = ["Nonrecursive";"Elimination";"Schemes"]; optread = (fun () -> !bifinite_elim_flag) ; optwrite = (fun b -> bifinite_elim_flag := b) } let _ = declare_bool_option - { optsync = true; - optdepr = true; (* compatibility 2014-09-03*) + { optdepr = true; (* compatibility 2014-09-03*) optname = "automatic declaration of induction schemes for non-recursive types"; optkey = ["Record";"Elimination";"Schemes"]; optread = (fun () -> !bifinite_elim_flag) ; @@ -73,8 +70,7 @@ let _ = let case_flag = ref false let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "automatic declaration of case analysis schemes"; optkey = ["Case";"Analysis";"Schemes"]; optread = (fun () -> !case_flag) ; @@ -83,16 +79,14 @@ let _ = let eq_flag = ref false let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "automatic declaration of boolean equality"; optkey = ["Boolean";"Equality";"Schemes"]; optread = (fun () -> !eq_flag) ; optwrite = (fun b -> eq_flag := b) } let _ = (* compatibility *) declare_bool_option - { optsync = true; - optdepr = true; + { optdepr = true; optname = "automatic declaration of boolean equality"; optkey = ["Equality";"Scheme"]; optread = (fun () -> !eq_flag) ; @@ -103,8 +97,7 @@ let is_eq_flag () = !eq_flag && Flags.version_strictly_greater Flags.V8_2 let eq_dec_flag = ref false let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "automatic declaration of decidable equality"; optkey = ["Decidable";"Equality";"Schemes"]; optread = (fun () -> !eq_dec_flag) ; @@ -113,8 +106,7 @@ let _ = let rewriting_flag = ref false let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname ="automatic declaration of rewriting schemes for equality types"; optkey = ["Rewriting";"Schemes"]; optread = (fun () -> !rewriting_flag) ; diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index b79795aeb..816cb2478 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -474,8 +474,7 @@ let keep_admitted_vars = ref true let _ = let open Goptions in declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "keep section variables in admitted proofs"; optkey = ["Keep"; "Admitted"; "Variables"]; optread = (fun () -> !keep_admitted_vars); diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 24cb9c886..c43816c9c 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -340,8 +340,7 @@ let get_hide_obligations () = !hide_obligations open Goptions let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "Hidding of Program obligations"; optkey = ["Hide";"Obligations"]; optread = get_hide_obligations; @@ -354,8 +353,7 @@ let get_shrink_obligations () = !shrink_obligations let _ = declare_bool_option - { optsync = true; - optdepr = true; + { optdepr = true; optname = "Shrinking of Program obligations"; optkey = ["Shrink";"Obligations"]; optread = get_shrink_obligations; diff --git a/vernac/record.ml b/vernac/record.ml index 53722b8f6..fabd11260 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -35,8 +35,7 @@ module RelDecl = Context.Rel.Declaration let primitive_flag = ref false let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "use of primitive projections"; optkey = ["Primitive";"Projections"]; optread = (fun () -> !primitive_flag) ; @@ -45,8 +44,7 @@ let _ = let typeclasses_strict = ref false let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "strict typeclass resolution"; optkey = ["Typeclasses";"Strict";"Resolution"]; optread = (fun () -> !typeclasses_strict); @@ -55,8 +53,7 @@ let _ = let typeclasses_unique = ref false let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "unique typeclass instances"; optkey = ["Typeclasses";"Unique";"Instances"]; optread = (fun () -> !typeclasses_unique); diff --git a/vernac/search.ml b/vernac/search.ml index 5b6e9a9c3..916015800 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -40,7 +40,6 @@ module SearchBlacklist = let title = "Current search blacklist : " let member_message s b = str "Search blacklist does " ++ (if b then mt () else str "not ") ++ str "include " ++ str s - let synchronous = true end) (* The functions iter_constructors and iter_declarations implement the behavior diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index d4e6af995..6c5b0dfb4 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1228,8 +1228,7 @@ let vernac_generalizable locality = let _ = declare_bool_option - { optsync = false; - optdepr = false; + { optdepr = false; optname = "silent"; optkey = ["Silent"]; optread = (fun () -> !Flags.quiet); @@ -1237,8 +1236,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "implicit arguments"; optkey = ["Implicit";"Arguments"]; optread = Impargs.is_implicit_args; @@ -1246,8 +1244,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "strict implicit arguments"; optkey = ["Strict";"Implicit"]; optread = Impargs.is_strict_implicit_args; @@ -1255,8 +1252,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "strong strict implicit arguments"; optkey = ["Strongly";"Strict";"Implicit"]; optread = Impargs.is_strongly_strict_implicit_args; @@ -1264,8 +1260,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "contextual implicit arguments"; optkey = ["Contextual";"Implicit"]; optread = Impargs.is_contextual_implicit_args; @@ -1273,8 +1268,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "implicit status of reversible patterns"; optkey = ["Reversible";"Pattern";"Implicit"]; optread = Impargs.is_reversible_pattern_implicit_args; @@ -1282,8 +1276,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "maximal insertion of implicit"; optkey = ["Maximal";"Implicit";"Insertion"]; optread = Impargs.is_maximal_implicit_args; @@ -1291,8 +1284,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "automatic introduction of variables"; optkey = ["Automatic";"Introduction"]; optread = Flags.is_auto_intros; @@ -1300,8 +1292,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "coercion printing"; optkey = ["Printing";"Coercions"]; optread = (fun () -> !Constrextern.print_coercions); @@ -1309,8 +1300,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "printing of existential variable instances"; optkey = ["Printing";"Existential";"Instances"]; optread = (fun () -> !Detyping.print_evar_arguments); @@ -1318,8 +1308,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "implicit arguments printing"; optkey = ["Printing";"Implicit"]; optread = (fun () -> !Constrextern.print_implicits); @@ -1327,8 +1316,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "implicit arguments defensive printing"; optkey = ["Printing";"Implicit";"Defensive"]; optread = (fun () -> !Constrextern.print_implicits_defensive); @@ -1336,8 +1324,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "projection printing using dot notation"; optkey = ["Printing";"Projections"]; optread = (fun () -> !Constrextern.print_projections); @@ -1345,8 +1332,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "notations printing"; optkey = ["Printing";"Notations"]; optread = (fun () -> not !Constrextern.print_no_symbol); @@ -1354,8 +1340,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "raw printing"; optkey = ["Printing";"All"]; optread = (fun () -> !Flags.raw_print); @@ -1363,8 +1348,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "use of the program extension"; optkey = ["Program";"Mode"]; optread = (fun () -> !Flags.program_mode); @@ -1372,8 +1356,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "universe polymorphism"; optkey = ["Universe"; "Polymorphism"]; optread = Flags.is_universe_polymorphism; @@ -1381,8 +1364,7 @@ let _ = let _ = declare_int_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "the level of inlining during functor application"; optkey = ["Inline";"Level"]; optread = (fun () -> Some (Flags.get_inline_level ())); @@ -1392,8 +1374,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "kernel term sharing"; optkey = ["Kernel"; "Term"; "Sharing"]; optread = (fun () -> !CClosure.share); @@ -1404,8 +1385,7 @@ let _ = let _ = declare_int_option - { optsync = false; - optdepr = true; + { optdepr = true; optname = "the undo limit (OBSOLETE)"; optkey = ["Undo"]; optread = (fun _ -> None); @@ -1413,8 +1393,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "display compact goal contexts"; optkey = ["Printing";"Compact";"Contexts"]; optread = (fun () -> Printer.get_compact_context()); @@ -1422,8 +1401,7 @@ let _ = let _ = declare_int_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "the printing depth"; optkey = ["Printing";"Depth"]; optread = Topfmt.get_depth_boxes; @@ -1431,8 +1409,7 @@ let _ = let _ = declare_int_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "the printing width"; optkey = ["Printing";"Width"]; optread = Topfmt.get_margin; @@ -1440,8 +1417,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "printing of universes"; optkey = ["Printing";"Universes"]; optread = (fun () -> !Constrextern.print_universes); @@ -1449,8 +1425,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "dumping bytecode after compilation"; optkey = ["Dump";"Bytecode"]; optread = Flags.get_dump_bytecode; @@ -1458,8 +1433,7 @@ let _ = let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "explicitly parsing implicit arguments"; optkey = ["Parsing";"Explicit"]; optread = (fun () -> !Constrintern.parsing_explicit); @@ -1467,8 +1441,7 @@ let _ = let _ = declare_string_option ~preprocess:CWarnings.normalize_flags_string - { optsync = true; - optdepr = false; + { optdepr = false; optname = "warnings display"; optkey = ["Warnings"]; optread = CWarnings.get_flags; @@ -1739,8 +1712,7 @@ let search_output_name_only = ref false let _ = declare_bool_option - { optsync = true; - optdepr = false; + { optdepr = false; optname = "output-name-only search"; optkey = ["Search";"Output";"Name";"Only"]; optread = (fun () -> !search_output_name_only); @@ -2137,8 +2109,7 @@ let default_timeout = ref None let _ = Goptions.declare_int_option - { Goptions.optsync = true; - Goptions.optdepr = false; + { Goptions.optdepr = false; Goptions.optname = "the default timeout"; Goptions.optkey = ["Default";"Timeout"]; Goptions.optread = (fun () -> !default_timeout); |