Added a DEPRECATED flag in declaration of options. For now only two options are declared as such, but I suspect Coq to contain some more.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14724 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 35 insertions, 0 deletions

diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index 34ecab2d5e..79ae41c1d0 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.ml
@@ -310,6 +310,7 @@ let end_autoinstance () =
 let _ =
   Goptions.declare_bool_option
     { Goptions.optsync=true;
+      Goptions.optdepr=false;
       Goptions.optkey=["Autoinstance"];
       Goptions.optname="automatic typeclass instance recognition";
       Goptions.optread=(fun () -> !autoinstance_opt);
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 489d28a4ec..e3779e131b 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -47,6 +47,7 @@ let elim_flag = ref true
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "automatic declaration of induction schemes";
       optkey   = ["Elimination";"Schemes"];
       optread  = (fun () -> !elim_flag) ;
@@ -56,6 +57,7 @@ let case_flag = ref true
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "automatic declaration of case analysis schemes";
       optkey   = ["Case";"Analysis";"Schemes"];
       optread  = (fun () -> !case_flag) ;
@@ -65,6 +67,7 @@ let eq_flag = ref false
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "automatic declaration of boolean equality";
       optkey   = ["Boolean";"Equality";"Schemes"];
       optread  = (fun () -> !eq_flag) ;
@@ -72,6 +75,7 @@ let _ =
 let _ = (* compatibility *)
   declare_bool_option
     { optsync  = true;
+      optdepr  = true;
       optname  = "automatic declaration of boolean equality";
       optkey   = ["Equality";"Scheme"];
       optread  = (fun () -> !eq_flag) ;
@@ -83,6 +87,7 @@ let eq_dec_flag = ref false
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "automatic declaration of decidable equality";
       optkey   = ["Decidable";"Equality";"Schemes"];
       optread  = (fun () -> !eq_dec_flag) ;
@@ -92,6 +97,7 @@ let rewriting_flag = ref false
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  ="automatic declaration of rewriting schemes for equality types";
       optkey   = ["Rewriting";"Schemes"];
       optread  = (fun () -> !rewriting_flag) ;
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 934cddb4f8..84e20f5eda 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -61,6 +61,7 @@ let default_timeout = ref None
 let _ =
   Goptions.declare_int_option
     { Goptions.optsync  = true;
+      Goptions.optdepr  = false;
       Goptions.optname  = "the default timeout";
       Goptions.optkey   = ["Default";"Timeout"];
       Goptions.optread  = (fun () -> !default_timeout);
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 8e370bc734..a38f7ce36d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -853,6 +853,7 @@ let make_silent_if_not_pcoq b =
 let _ =
   declare_bool_option
     { optsync  = false;
+      optdepr  = false;
       optname  = "silent";
       optkey   = ["Silent"];
       optread  = is_silent;
@@ -861,6 +862,7 @@ let _ =
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "implicit arguments";
       optkey   = ["Implicit";"Arguments"];
       optread  = Impargs.is_implicit_args;
@@ -869,6 +871,7 @@ let _ =
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "strict implicit arguments";
       optkey   = ["Strict";"Implicit"];
       optread  = Impargs.is_strict_implicit_args;
@@ -877,6 +880,7 @@ let _ =
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "strong strict implicit arguments";
       optkey   = ["Strongly";"Strict";"Implicit"];
       optread  = Impargs.is_strongly_strict_implicit_args;
@@ -885,6 +889,7 @@ let _ =
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "contextual implicit arguments";
       optkey   = ["Contextual";"Implicit"];
       optread  = Impargs.is_contextual_implicit_args;
@@ -893,6 +898,7 @@ let _ =
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "implicit status of reversible patterns";
       optkey   = ["Reversible";"Pattern";"Implicit"];
       optread  = Impargs.is_reversible_pattern_implicit_args;
@@ -901,6 +907,7 @@ let _ =
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "maximal insertion of implicit";
       optkey   = ["Maximal";"Implicit";"Insertion"];
       optread  = Impargs.is_maximal_implicit_args;
@@ -909,6 +916,7 @@ let _ =
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "automatic introduction of variables";
       optkey   = ["Automatic";"Introduction"];
       optread  = Flags.is_auto_intros;
@@ -917,6 +925,7 @@ let _ =
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "coercion printing";
       optkey   = ["Printing";"Coercions"];
       optread  = (fun () -> !Constrextern.print_coercions);
@@ -925,6 +934,7 @@ let _ =
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "printing of existential variable instances";
       optkey   = ["Printing";"Existential";"Instances"];
       optread  = (fun () -> !Constrextern.print_evar_arguments);
@@ -932,6 +942,7 @@ let _ =
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "implicit arguments printing";
       optkey   = ["Printing";"Implicit"];
       optread  = (fun () -> !Constrextern.print_implicits);
@@ -940,6 +951,7 @@ let _ =
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "implicit arguments defensive printing";
       optkey   = ["Printing";"Implicit";"Defensive"];
       optread  = (fun () -> !Constrextern.print_implicits_defensive);
@@ -948,6 +960,7 @@ let _ =
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "projection printing using dot notation";
       optkey   = ["Printing";"Projections"];
       optread  = (fun () -> !Constrextern.print_projections);
@@ -956,6 +969,7 @@ let _ =
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "notations printing";
       optkey   = ["Printing";"Notations"];
       optread  = (fun () -> not !Constrextern.print_no_symbol);
@@ -964,6 +978,7 @@ let _ =
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "raw printing";
       optkey   = ["Printing";"All"];
       optread  = (fun () -> !Flags.raw_print);
@@ -972,6 +987,7 @@ let _ =
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "record printing";
       optkey   = ["Printing";"Records"];
       optread  = (fun () -> !Flags.record_print);
@@ -980,6 +996,7 @@ let _ =
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "use of virtual machine inside the kernel";
       optkey   = ["Virtual";"Machine"];
       optread  = (fun () -> Vconv.use_vm ());
@@ -988,6 +1005,7 @@ let _ =
 let _ =
   declare_int_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "the level of inling duging functor application";
       optkey   = ["Inline";"Level"];
       optread  = (fun () -> Some (Flags.get_inline_level ()));
@@ -998,6 +1016,7 @@ let _ =
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "use of boxed values";
       optkey   = ["Boxed";"Values"];
       optread  = (fun _ -> not (Vm.transp_values ()));
@@ -1009,6 +1028,7 @@ let _ =
 let _ =
   declare_int_option
     { optsync  = false;
+      optdepr  = true;
       optname  = "the undo limit (OBSOLETE)";
       optkey   = ["Undo"];
       optread  = (fun _ -> None);
@@ -1017,6 +1037,7 @@ let _ =
 let _ =
   declare_int_option
     { optsync  = false;
+      optdepr  = false;
       optname  = "the hypotheses limit";
       optkey   = ["Hyps";"Limit"];
       optread  = Flags.print_hyps_limit;
@@ -1025,6 +1046,7 @@ let _ =
 let _ =
   declare_int_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "the printing depth";
       optkey   = ["Printing";"Depth"];
       optread  = Pp_control.get_depth_boxes;
@@ -1033,6 +1055,7 @@ let _ =
 let _ =
   declare_int_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "the printing width";
       optkey   = ["Printing";"Width"];
       optread  = Pp_control.get_margin;
@@ -1041,6 +1064,7 @@ let _ =
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "printing of universes";
       optkey   = ["Printing";"Universes"];
       optread  = (fun () -> !Constrextern.print_universes);
@@ -1052,6 +1076,7 @@ let vernac_debug b =
 let _ =
   declare_bool_option
     { optsync  = false;
+      optdepr  = false;
       optname  = "Ltac debug";
       optkey   = ["Ltac";"Debug"];
       optread  = (fun () -> get_debug () <> Tactic_debug.DebugOff);
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 3fd114afe0..aa38e9e9f4 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -38,6 +38,7 @@ open Goptions
 let _ =
   declare_string_option
     { optsync  = false;
+      optdepr  = false;
       optname  = "Whelp server";
       optkey   = ["Whelp";"Server"];
       optread  = (fun () -> !whelp_server_name);
@@ -46,6 +47,7 @@ let _ =
 let _ =
   declare_string_option
     { optsync  = false;
+      optdepr  = false;
       optname  = "Whelp getter";
       optkey   = ["Whelp";"Getter"];
       optread  = (fun () -> !getter_server_name);