Deprecate options that were introduced for compatibility with 8.5.

5 files changed, 15 insertions, 14 deletions

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index cc1709f1c2..ce9ca93d90 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -29,7 +29,7 @@ exception Elimconst
 
 let refolding_in_reduction = ref false
 let _ = Goptions.declare_bool_option {
-  Goptions.optdepr = false;
+  Goptions.optdepr = true; (* remove in 8.8 *)
   Goptions.optname =
     "Perform refolding of fixpoints/constants like cbn during reductions";
   Goptions.optkey = ["Refolding";"Reduction"];
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 7a85956538..9cf2f0bc0c 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -92,7 +92,7 @@ open Goptions
 
 let _ =
   declare_bool_option
-    { optdepr  = true;
+    { optdepr  = true; (* remove in 8.8 *)
       optname  = "do typeclass search modulo eta conversion";
       optkey   = ["Typeclasses";"Modulo";"Eta"];
       optread  = get_typeclasses_modulo_eta;
@@ -125,7 +125,7 @@ let _ =
 
 let _ =
   declare_bool_option
-    { optdepr  = false;
+    { optdepr  = true; (* remove in 8.8 *)
       optname  = "compat";
       optkey   = ["Typeclasses";"Legacy";"Resolution"];
       optread  = get_typeclasses_legacy_resolution;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2e3a4e33b3..6f2baed905 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -80,15 +80,15 @@ let _ =
       optread  = (fun () -> !Flags.tactic_context_compat) ;
       optwrite = (fun b -> Flags.tactic_context_compat := b) }
 
-let apply_solve_class_goals = ref (false)
-let _ = Goptions.declare_bool_option {
-  Goptions.optdepr = true;
-  Goptions.optname =
-    "Perform typeclass resolution on apply-generated subgoals.";
-  Goptions.optkey = ["Typeclass";"Resolution";"After";"Apply"];
-  Goptions.optread = (fun () -> !apply_solve_class_goals);
-  Goptions.optwrite = (fun a -> apply_solve_class_goals:=a);
-}
+let apply_solve_class_goals = ref false
+
+let _ =
+  declare_bool_option
+    { optdepr = true; (* remove in 8.8 *)
+      optname = "Perform typeclass resolution on apply-generated subgoals.";
+      optkey = ["Typeclass";"Resolution";"After";"Apply"];
+      optread = (fun () -> !apply_solve_class_goals);
+      optwrite = (fun a -> apply_solve_class_goals := a); }
 
 let clear_hyp_by_default = ref false
 
@@ -124,7 +124,7 @@ let shrink_abstract = ref true
 
 let _ =
   declare_bool_option
-    { optdepr  = true;
+    { optdepr  = true; (* remove in 8.8 *)
       optname  = "shrinking of abstracted proofs";
       optkey   = ["Shrink"; "Abstract"];
       optread  = (fun () -> !shrink_abstract) ;
diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v
index f761a4dc5a..73169dae65 100644
--- a/test-suite/output/inference.v
+++ b/test-suite/output/inference.v
@@ -14,6 +14,7 @@ Definition P (e:option L) :=
 Print P.
 
 (* Check that plus is folded even if reduction is involved *)
+Set Warnings Append "-deprecated-option".
 Set Refolding Reduction.
 Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H).
 
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index c0acdaf57d..5647a9c4f7 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -350,7 +350,7 @@ let get_shrink_obligations () = !shrink_obligations
 
 let _ =
   declare_bool_option
-    { optdepr  = true;
+    { optdepr  = true; (* remove in 8.8 *)
       optname  = "Shrinking of Program obligations";
       optkey   = ["Shrink";"Obligations"];
       optread  = get_shrink_obligations;