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

6 files changed, 12 insertions, 0 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 142c286195..e3d27f7191 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 6bcda00978..229f72a269 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 75584ead38..567b0727cd 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 c1b7b63c3e..4a38c48dcf 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 951b25baf2..233cdddd7f 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 74ee05bbc6..a719a9f9af 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;