From fbbcea2eda411fbacfafdeec3266a19af17935f3 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 4 Jul 2017 17:11:45 +0200
Subject: Deprecate options that were introduced for compatibility with 8.5.

---
 pretyping/reductionops.ml     |  2 +-
 tactics/class_tactics.ml      |  4 ++--
 tactics/tactics.ml            | 20 ++++++++++----------
 test-suite/output/inference.v |  1 +
 vernac/obligations.ml         |  2 +-
 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;
-- 
cgit v1.2.3


From 2b4616438cc2a41e2c381ad47819d13addbd773c Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 11 Jul 2017 17:16:15 +0200
Subject: Backtracking on deprecation of Bracketing Last Intro Pattern.

As per @JasonGross's request who described a use case for this option in
https://coq.inria.fr/bugs/show_bug.cgi?id=5633 and pending an alternative
solution for this use case.
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 6f2baed905..1c60010cad 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -143,7 +143,7 @@ let use_bracketing_last_or_and_intro_pattern () =
 
 let _ =
   declare_bool_option
-    { optdepr  = true; (* remove in 8.8 *)
+    { optdepr  = false;
       optname  = "bracketing last or-and introduction pattern";
       optkey   = ["Bracketing";"Last";"Introduction";"Pattern"];
       optread  = (fun () -> !bracketing_last_or_and_intro_pattern);
-- 
cgit v1.2.3


From fe56933b466a3d833d161828a34aab7a6b621b00 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 11 Jul 2017 17:52:22 +0200
Subject: Sync the manual with the deprecation warnings.

---
 doc/refman/Classes.tex     | 6 ++++--
 doc/refman/Program.tex     | 3 ++-
 doc/refman/RefMan-ltac.tex | 3 ++-
 doc/refman/RefMan-tac.tex  | 1 +
 4 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index 5966ac468c..7e07868a38 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -486,15 +486,17 @@ where there is a hole in that place.
 
 \subsection{\tt Set Typeclasses Legacy Resolution}
 \optindex{Typeclasses Legacy Resolution}
+\emph{Deprecated since 8.7}
 
 This option (off by default) uses the 8.5 implementation of resolution.
 Use for compatibility purposes only (porting and debugging).
 
 \subsection{\tt Set Typeclasses Module Eta}
 \optindex{Typeclasses Modulo Eta}
+\emph{Deprecated since 8.7}
 
 This option allows eta-conversion for functions and records during
-unification of type-classes. This option is now unsupported in 8.6 with
+unification of type-classes. This option is unsupported since 8.6 with
 {\tt Typeclasses Filtered Unification} set, but still affects the
 default unification strategy, and the one used in {\tt Legacy
   Resolution} mode. It is \emph{unset} by default. If {\tt Typeclasses
@@ -505,7 +507,7 @@ pattern-matching is not up-to eta.
 \subsection{\tt Set Typeclasses Limit Intros}
 \optindex{Typeclasses Limit Intros}
 
-This option (on by default in Coq 8.6 and below) controls the ability to
+This option (on by default) controls the ability to
 apply hints while avoiding (functional) eta-expansions in the generated
 proof term. It does so by allowing hints that conclude in a product to
 apply to a goal with a matching product directly, avoiding an
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index 2fc1c8764a..f60908da6c 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -278,7 +278,8 @@ tactic is replaced by the default one if not specified.
   as implicit arguments of the special constant
   \texttt{Program.Tactics.obligation}.
 \item {\tt Set Shrink Obligations}\optindex{Shrink Obligations}
-  Control whether obligations should have their
+\emph{Deprecated since 8.7}
+  This option (on by default) controls whether obligations should have their
   context minimized to the set of variables used in the proof of the
   obligation, to avoid unnecessary dependencies.
 \end{itemize}
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex
index f3bc2dd05e..3ce1d4ecd8 100644
--- a/doc/refman/RefMan-ltac.tex
+++ b/doc/refman/RefMan-ltac.tex
@@ -1131,8 +1131,9 @@ on. This can be obtained thanks to the option below.
 \optindex{Shrink Abstract}
 {\tt Set Shrink Abstract}
 \end{quote}
+\emph{Deprecated since 8.7}
 
-When set, all lemmas generated through \texttt{abstract {\tacexpr}}
+When set (default), all lemmas generated through \texttt{abstract {\tacexpr}}
 and \texttt{transparent\_abstract {\tacexpr}} are quantified only over the
 variables that appear in the term constructed by \texttt{\tacexpr}.
 
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index ecb89b5fb8..a23c432322 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3485,6 +3485,7 @@ reduced to \texttt{S t}.
 \optindex{Refolding Reduction}
 {\tt Refolding Reduction}
 \end{quote}
+\emph{Deprecated since 8.7}
 
 This option (off by default) controls the use of the refolding strategy
 of {\tt cbn} while doing reductions in unification, type inference and
-- 
cgit v1.2.3