diff options
Diffstat (limited to 'plugins/extraction/table.ml')
| -rw-r--r-- | plugins/extraction/table.ml | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 7b64706138..a53c2395f0 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -503,7 +503,6 @@ let my_bool_option name initval = let access = fun () -> !flag in let () = declare_bool_option {optdepr = false; - optname = "Extraction "^name; optkey = ["Extraction"; name]; optread = access; optwrite = (:=) flag } @@ -575,14 +574,12 @@ let optims () = !opt_flag_ref let () = declare_bool_option {optdepr = false; - optname = "Extraction Optimize"; optkey = ["Extraction"; "Optimize"]; optread = (fun () -> not (Int.equal !int_flag_ref 0)); optwrite = (fun b -> chg_flag (if b then int_flag_init else 0))} let () = declare_int_option { optdepr = false; - optname = "Extraction Flag"; optkey = ["Extraction";"Flag"]; optread = (fun _ -> Some !int_flag_ref); optwrite = (function @@ -596,7 +593,6 @@ let conservative_types () = !conservative_types_ref let () = declare_bool_option {optdepr = false; - optname = "Extraction Conservative Types"; optkey = ["Extraction"; "Conservative"; "Types"]; optread = (fun () -> !conservative_types_ref); optwrite = (fun b -> conservative_types_ref := b) } @@ -608,7 +604,6 @@ let file_comment () = !file_comment_ref let () = declare_string_option {optdepr = false; - optname = "Extraction File Comment"; optkey = ["Extraction"; "File"; "Comment"]; optread = (fun () -> !file_comment_ref); optwrite = (fun s -> file_comment_ref := s) } |