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

22 files changed, 82 insertions, 16 deletions

diff --git a/library/goptions.ml b/library/goptions.ml
index 75fba89fe..7ba1d5189 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -206,6 +206,7 @@ module MakeRefTable =
 
 type 'a option_sig = {
   optsync  : bool;
+  optdepr  : bool;
   optname  : string;
   optkey   : option_name;
   optread  : unit -> 'a;
@@ -235,7 +236,7 @@ open Libobject
 open Lib
 
 let declare_option cast uncast
-  { optsync=sync; optname=name; optkey=key; optread=read; optwrite=write } =
+  { optsync=sync; optdepr=depr; optname=name; optkey=key; optread=read; optwrite=write } =
   check_key key;
   let default = read() in
   (* spiwack: I use two spaces in the nicknames of "local" and "global" objects.
@@ -274,7 +275,7 @@ let declare_option cast uncast
   let cwrite v = write (uncast v) in
   let clwrite v = lwrite (uncast v) in
   let cgwrite v = gwrite (uncast v) in
-  value_tab := OptionMap.add key (name,(sync,cread,cwrite,clwrite,cgwrite)) !value_tab;
+  value_tab := OptionMap.add key (name, depr, (sync,cread,cwrite,clwrite,cgwrite)) !value_tab;
   write
 
 type 'a write_function = 'a -> unit
@@ -297,7 +298,7 @@ let declare_string_option =
 (* Setting values of options *)
 
 let set_option_value locality check_and_cast key v =
-  let (name,(_,read,write,lwrite,gwrite)) =
+  let (name, depr, (_,read,write,lwrite,gwrite)) =
     try get_option key
     with Not_found -> error ("There is no option "^(nickname key)^".")
   in
@@ -358,7 +359,7 @@ let msg_option_value (name,v) =
 (*     | IdentValue r    -> pr_global_env Idset.empty r *)
 
 let print_option_value key =
-  let (name,(_,read,_,_,_)) = get_option key in
+  let (name, depr, (_,read,_,_,_)) = get_option key in
   let s = read () in
   match s with
     | BoolValue b ->
@@ -370,24 +371,23 @@ let print_option_value key =
 
 
 let print_tables () =
+  let print_option key name value depr =
+    let msg = str ("  "^(nickname key)^": ") ++ msg_option_value (name, value) in
+    if depr then msg ++ str " [DEPRECATED]" ++ fnl ()
+    else msg ++ fnl ()
+  in
   msg
     (str "Synchronous options:" ++ fnl () ++
      OptionMap.fold
-       (fun key (name,(sync,read,_,_,_)) p ->
-	  if sync then
-	    p ++ str ("  "^(nickname key)^": ") ++
-	    msg_option_value (name,read()) ++ fnl ()
-	  else
-	    p)
+       (fun key (name, depr, (sync,read,_,_,_)) p ->
+	  if sync then p ++ print_option key name (read ()) depr
+	  else p)
        !value_tab (mt ()) ++
      str "Asynchronous options:" ++ fnl () ++
      OptionMap.fold
-       (fun key (name,(sync,read,_,_,_)) p ->
-	  if sync then
-	    p
-	  else
-	    p ++ str ("  "^(nickname key)^": ") ++
-            msg_option_value (name,read()) ++ fnl ())
+       (fun key (name, depr, (sync,read,_,_,_)) p ->
+	  if sync then p
+	  else p ++ print_option key name (read ()) depr)
        !value_tab (mt ()) ++
      str "Tables:" ++ fnl () ++
      List.fold_right
diff --git a/library/goptions.mli b/library/goptions.mli
index 1a89961ac..37c03f1bf 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -117,8 +117,13 @@ module MakeRefTable :
 
 type 'a option_sig = {
   optsync    : bool;
+  (** whether the option is synchronous w.r.t to the section/module system. *)
+  optdepr    : bool;
+  (** whether the option is DEPRECATED *)
   optname    : string;
+  (** a short string describing the option *)
   optkey     : option_name;
+  (** the low-level name of this option *)
   optread    : unit -> 'a;
   optwrite   : 'a -> unit
 }
diff --git a/parsing/printmod.ml b/parsing/printmod.ml
index cf2aad203..9cf76585e 100644
--- a/parsing/printmod.ml
+++ b/parsing/printmod.ml
@@ -28,6 +28,7 @@ let short = ref false
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "short module printing";
       optkey   = ["Short";"Module";"Printing"];
       optread  = (fun () -> !short) ;
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 142c28619..e3d27f719 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -28,6 +28,7 @@ let debug f x =
 let _=
   let gdopt=
     { optsync=true;
+      optdepr=false;
       optname="Congruence Verbose";
       optkey=["Congruence";"Verbose"];
       optread=(fun ()-> !cc_verbose);
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 6bcda0097..229f72a26 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -41,6 +41,7 @@ let get_strictness,set_strictness =
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "strict mode";
       optkey   = ["Strict";"Proofs"];
       optread  = get_strictness;
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 75584ead3..567b0727c 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -398,6 +398,7 @@ let my_bool_option name initval =
   let access = fun () -> !flag in
   let _ = declare_bool_option
     {optsync = true;
+     optdepr = false;
      optname = "Extraction "^name;
      optkey = ["Extraction"; name];
      optread = access;
@@ -470,6 +471,7 @@ let optims () = !opt_flag_ref
 
 let _ = declare_bool_option
 	  {optsync = true;
+           optdepr = false;
 	   optname = "Extraction Optimize";
 	   optkey = ["Extraction"; "Optimize"];
 	   optread = (fun () -> !int_flag_ref <> 0);
@@ -477,6 +479,7 @@ let _ = declare_bool_option
 
 let _ = declare_int_option
           { optsync = true;
+            optdepr = false;
             optname = "Extraction Flag";
             optkey = ["Extraction";"Flag"];
             optread = (fun _ -> Some !int_flag_ref);
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index c1b7b63c3..4a38c48dc 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -27,6 +27,7 @@ let ground_depth=ref 3
 let _=
   let gdopt=
     { optsync=true;
+      optdepr=false;
       optname="Firstorder Depth";
       optkey=["Firstorder";"Depth"];
       optread=(fun ()->Some !ground_depth);
@@ -42,6 +43,7 @@ let congruence_depth=ref 100
 let _=
   let gdopt=
     { optsync=true;
+      optdepr=false;
       optname="Congruence Depth";
       optkey=["Congruence";"Depth"];
       optread=(fun ()->Some !congruence_depth);
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 951b25baf..233cdddd7 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -451,6 +451,7 @@ open Goptions
 let functional_induction_rewrite_dependent_proofs_sig = 
   {
     optsync = false;
+    optdepr = false;
     optname = "Functional Induction Rewrite Dependent";
     optkey =  ["Functional";"Induction";"Rewrite";"Dependent"];
     optread = (fun () -> !functional_induction_rewrite_dependent_proofs);
@@ -463,6 +464,7 @@ let do_rewrite_dependent () = !functional_induction_rewrite_dependent_proofs = t
 let function_debug_sig =
   {
     optsync = false;
+    optdepr = false;
     optname = "Function debug";
     optkey =  ["Function_debug"];
     optread = (fun () -> !function_debug);
@@ -482,6 +484,7 @@ let is_strict_tcc () = !strict_tcc
 let strict_tcc_sig =
   {
     optsync = false;
+    optdepr = false;
     optname = "Raw Function Tcc";
     optkey =  ["Function_raw_tcc"];
     optread = (fun () -> !strict_tcc);
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 74ee05bbc..a719a9f9a 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -82,6 +82,7 @@ open Goptions
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "transparency of Program obligations";
       optkey   = ["Transparent";"Obligations"];
       optread  = get_proofs_transparency;
@@ -98,6 +99,7 @@ open Goptions
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "Hidding of Program obligations";
       optkey   = ["Hide";"Obligations"];
       optread  = get_hide_obligations;
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 03ae6e763..fe4d0f300 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -349,6 +349,7 @@ open Goptions
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "automatic import of coercions";
       optkey   = ["Automatic";"Coercions";"Import"];
       optread  = (fun () -> !automatically_import_coercions);
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 35aedd2c6..c194a0f23 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -116,6 +116,7 @@ let force_wildcard () = !wildcard_value
 
 let _ = declare_bool_option
 	  { optsync  = true;
+            optdepr  = false;
 	    optname  = "forced wildcard";
 	    optkey   = ["Printing";"Wildcard"];
 	    optread  = force_wildcard;
@@ -126,6 +127,7 @@ let synthetize_type () = !synth_type_value
 
 let _ = declare_bool_option
 	  { optsync  = true;
+            optdepr  = false;
 	    optname  = "pattern matching return type synthesizability";
 	    optkey   = ["Printing";"Synth"];
 	    optread  = synthetize_type;
@@ -136,6 +138,7 @@ let reverse_matching () = !reverse_matching_value
 
 let _ = declare_bool_option
 	  { optsync  = true;
+            optdepr  = false;
 	    optname  = "pattern-matching reversibility";
 	    optkey   = ["Printing";"Matching"];
 	    optread  = reverse_matching;
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 9f7b6d748..187533ad3 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -175,6 +175,7 @@ open Goptions
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "pattern-unification for existential variables in tactics";
       optkey   = ["Tactic";"Evars";"Pattern";"Unification"];
       optread  = (fun () -> !global_evars_pattern_unification_flag);
@@ -183,6 +184,7 @@ let _ =
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "pattern-unification for existential variables in tactics";
       optkey   = ["Tactic";"Pattern";"Unification"];
       optread  = (fun () -> !global_evars_pattern_unification_flag);
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 99552c552..e9af46ba9 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -45,6 +45,7 @@ let default_proof_mode = ref standard
 let _ =
   Goptions.declare_string_option {Goptions.
     optsync = true ;
+    optdepr = false;
     optname = "default proof mode" ;
     optkey = ["Default";"Proof";"Mode"] ;
     optread = begin fun () -> 
@@ -386,6 +387,7 @@ module Bullet = struct
   let _ =
     Goptions.declare_string_option {Goptions.
       optsync = true;
+      optdepr = false;
       optname = "bullet behavior";
       optkey = ["Bullet";"Behavior"];
       optread = begin fun () ->
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index c33299397..82b426775 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -694,6 +694,7 @@ let get_typeclasses_debug () = !typeclasses_debug
 let set_typeclasses_debug =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "debug output for typeclasses proof search";
       optkey   = ["Typeclasses";"Debug"];
       optread  = get_typeclasses_debug;
@@ -708,6 +709,7 @@ let get_typeclasses_depth () = !typeclasses_depth
 let set_typeclasses_depth =
   declare_int_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "depth for typeclasses proof search";
       optkey   = ["Typeclasses";"Depth"];
       optread  = get_typeclasses_depth;
diff --git a/tactics/equality.ml b/tactics/equality.ml
index b037ea7e2..76bceb738 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -56,6 +56,7 @@ open Goptions
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "automatic introduction of hypotheses by discriminate";
       optkey   = ["Discriminate";"Introduction"];
       optread  = (fun () -> !discriminate_introduction);
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cddb7a2b2..25a148bbd 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -72,6 +72,7 @@ let use_dependent_propositions_elimination () =
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "dependent-propositions-elimination tactic";
       optkey   = ["Dependent";"Propositions";"Elimination"];
       optread  = (fun () -> !dependent_propositions_elimination) ;
diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index 46f8c9bb4..b7a58be45 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -53,6 +53,7 @@ open Goptions
 let _ =
   declare_bool_option
     { optsync  = true;
+      optdepr  = false;
       optname  = "unfolding of iff and not in intuition";
       optkey   = ["Intuition";"Iff";"Unfolding"];
       optread  = (fun () -> !iff_unfolding);
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index 34ecab2d5..79ae41c1d 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 489d28a4e..e3779e131 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 934cddb4f..84e20f5ed 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 8e370bc73..a38f7ce36 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 3fd114afe..aa38e9e9f 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);