Deprecate options that were introduced for compatibility with 8.5.

1 files changed, 10 insertions, 10 deletions

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) ;