Merge PR#375: Deprecation

26 files changed, 50 insertions, 361 deletions

diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 1b847414f..48f82f2d9 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -589,7 +589,6 @@ through the <tt>Require Import</tt> command.</p>
   </dt>
   <dd>
     theories/Compat/AdmitAxiom.v
-    theories/Compat/Coq84.v
     theories/Compat/Coq85.v
     theories/Compat/Coq86.v
   </dd>
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 5bd62273c..783085654 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -412,13 +412,12 @@ let rename_bound_vars_as_displayed sigma avoid env c =
 
 let h_based_elimination_names = ref false
 
-let use_h_based_elimination_names () =
-  !h_based_elimination_names && Flags.version_strictly_greater Flags.V8_4
+let use_h_based_elimination_names () = !h_based_elimination_names
 
 open Goptions
 
 let _ = declare_bool_option
-	  { optdepr  = false;
+	  { optdepr  = true; (* remove in 8.8 *)
 	    optname  = "use of \"H\"-based proposition names in elimination tactics";
 	    optkey   = ["Standard";"Proposition";"Elimination";"Names"];
 	    optread  = (fun () -> !h_based_elimination_names);
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 3d484a02d..67fee6202 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -786,7 +786,7 @@ let find_appl_head_data c =
     let scopes = find_arguments_scope ref in
       c, impls, scopes, []
   | GApp ({ v = GRef (ref,_) },l)
-      when l != [] && Flags.version_strictly_greater Flags.V8_2 ->
+      when l != [] ->
       let n = List.length l in
       let impls = implicits_of_global ref in 
       let scopes = find_arguments_scope ref in
diff --git a/lib/flags.ml b/lib/flags.ml
index 6a3b7a426..13539bced 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -106,35 +106,27 @@ let we_are_parsing = ref false
 (* Current means no particular compatibility consideration.
    For correct comparisons, this constructor should remain the last one. *)
 
-type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | V8_6 | Current
+type compat_version = VOld | V8_5 | V8_6 | Current
 
 let compat_version = ref Current
 
 let version_compare v1 v2 = match v1, v2 with
-| V8_2, V8_2 -> 0
-| V8_2, (V8_3 | V8_4 | V8_5 | V8_6 | Current) -> -1
-| V8_3, V8_2 -> 1
-| V8_3, V8_3 -> 0
-| V8_3, (V8_4 | V8_5 | V8_6 | Current) -> -1
-| V8_4, (V8_2 | V8_3) -> 1
-| V8_4, V8_4 -> 0
-| V8_4, (V8_5 | V8_6 | Current) -> -1
-| V8_5, (V8_2 | V8_3 | V8_4) -> 1
-| V8_5, V8_5 -> 0
-| V8_5, (V8_6 | Current) -> -1
-| V8_6, (V8_2 | V8_3 | V8_4 | V8_5) -> 1
-| V8_6, V8_6 -> 0
-| V8_6, Current -> -1
-| Current, Current -> 0
-| Current, (V8_2 | V8_3 | V8_4 | V8_5 | V8_6) -> 1
+  | VOld, VOld -> 0
+  | VOld, _ -> -1
+  | _, VOld -> 1
+  | V8_5, V8_5 -> 0
+  | V8_5, _ -> -1
+  | _, V8_5 -> 1
+  | V8_6, V8_6 -> 0
+  | V8_6, _ -> -1
+  | _, V8_6 -> 1
+  | Current, Current -> 0
 
 let version_strictly_greater v = version_compare !compat_version v > 0
 let version_less_or_equal v = not (version_strictly_greater v)
 
 let pr_version = function
-  | V8_2 -> "8.2"
-  | V8_3 -> "8.3"
-  | V8_4 -> "8.4"
+  | VOld -> "old"
   | V8_5 -> "8.5"
   | V8_6 -> "8.6"
   | Current -> "current"
@@ -157,7 +149,7 @@ let is_verbose () = not !quiet
 
 let auto_intros = ref true
 let make_auto_intros flag = auto_intros := flag
-let is_auto_intros () = version_strictly_greater V8_2 && !auto_intros
+let is_auto_intros () = !auto_intros
 
 let universe_polymorphism = ref false
 let make_universe_polymorphism b = universe_polymorphism := b
diff --git a/lib/flags.mli b/lib/flags.mli
index e2cf09474..0026aba2e 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -77,7 +77,7 @@ val raw_print : bool ref
 (* Univ print flag, never set anywere. Maybe should belong to Univ? *)
 val univ_print : bool ref
 
-type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | V8_6 | Current
+type compat_version = VOld | V8_5 | V8_6 | Current
 val compat_version : compat_version ref
 val version_compare : compat_version -> compat_version -> int
 val version_strictly_greater : compat_version -> bool
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 5eacb1a95..2a8ed7238 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -66,7 +66,7 @@ let negation_unfolding = ref true
 (* Whether inner iff are unfolded *)
 let iff_unfolding = ref false
 
-let unfold_iff () = !iff_unfolding || Flags.version_less_or_equal Flags.V8_2
+let unfold_iff () = !iff_unfolding
 
 open Goptions
 let _ =
@@ -79,7 +79,7 @@ let _ =
 
 let _ =
   declare_bool_option
-    { optdepr  = false;
+    { optdepr  = true; (* remove in 8.8 *)
       optname  = "unfolding of iff in intuition";
       optkey   = ["Intuition";"Iff";"Unfolding"];
       optread  = (fun () -> !iff_unfolding);
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 9a973cff5..8d87f6e99 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -428,7 +428,7 @@ let automatically_import_coercions = ref false
 open Goptions
 let _ =
   declare_bool_option
-    { optdepr  = false;
+    { optdepr  = true; (* remove in 8.8 *)
       optname  = "automatic import of coercions";
       optkey   = ["Automatic";"Coercions";"Import"];
       optread  = (fun () -> !automatically_import_coercions);
@@ -454,15 +454,11 @@ let cache_coercion (_, c) =
   add_coercion_in_graph (xf,is,it)
 
 let load_coercion _ o =
-  if
-    !automatically_import_coercions || Flags.version_less_or_equal Flags.V8_2
-  then
+  if !automatically_import_coercions then
     cache_coercion o
 
 let open_coercion i o =
-  if Int.equal i 1 && not
-    (!automatically_import_coercions || Flags.version_less_or_equal Flags.V8_2)
-  then
+  if Int.equal i 1 && not !automatically_import_coercions then
     cache_coercion o
 
 let subst_coercion (subst, c) =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 0fb48ed8c..67c8b07e7 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -248,24 +248,13 @@ let sort_eqns = unify_r2l
 
 let global_pattern_unification_flag = ref true
 
-(* Compatibility option introduced and activated in Coq 8.3 whose
-   syntax is now deprecated. *)
-
 open Goptions
-let _ =
-  declare_bool_option
-    { optdepr  = true;
-      optname  = "pattern-unification for existential variables in tactics";
-      optkey   = ["Tactic";"Evars";"Pattern";"Unification"];
-      optread  = (fun () -> !global_pattern_unification_flag);
-      optwrite = (:=) global_pattern_unification_flag }
 
-(* Compatibility option superseding the previous one, introduced and
-   activated in Coq 8.4 *)
+(* Compatibility option introduced and activated in Coq 8.4 *)
 
 let _ =
   declare_bool_option
-    { optdepr  = false;
+    { optdepr  = true; (* remove in 8.8 *)
       optname  = "pattern-unification for existential variables in tactics";
       optkey   = ["Tactic";"Pattern";"Unification"];
       optread  = (fun () -> !global_pattern_unification_flag);
@@ -481,12 +470,10 @@ let set_flags_for_type flags = { flags with
 
 let use_evars_pattern_unification flags =
   !global_pattern_unification_flag && flags.use_pattern_unification
-  && Flags.version_strictly_greater Flags.V8_2
 
 let use_metas_pattern_unification sigma flags nb l =
   !global_pattern_unification_flag && flags.use_pattern_unification
-  || (Flags.version_less_or_equal Flags.V8_3 || 
-      flags.use_meta_bound_pattern_unification) &&
+  || flags.use_meta_bound_pattern_unification &&
      Array.for_all (fun c -> isRel sigma c && destRel sigma c <= nb) l
 
 type key = 
@@ -609,9 +596,6 @@ let do_reduce ts (env, nb) sigma c =
   Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state
 		  ts env sigma Cst_stack.empty (c, Stack.empty)))
 
-let use_full_betaiota flags =
-  flags.modulo_betaiota && Flags.version_strictly_greater Flags.V8_3
-
 let isAllowedEvar sigma flags c = match EConstr.kind sigma c with
   | Evar (evk,_) -> not (Evar.Set.mem evk flags.frozen_evars)
   | _ -> false
@@ -949,7 +933,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
 	  expand curenvnb pb opt substn cM f1 l1 cN f2 l2
 
   and reduce curenvnb pb opt (sigma, metas, evars as substn) cM cN =
-    if use_full_betaiota flags && not (subterm_restriction opt flags) then
+    if flags.modulo_betaiota && not (subterm_restriction opt flags) then
       let cM' = do_reduce flags.modulo_delta curenvnb sigma cM in
 	if not (EConstr.eq_constr sigma cM cM') then
 	  unirec_rec curenvnb pb opt substn cM' cN
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 05c5cd5ec..6e56dc48e 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -50,13 +50,12 @@ module NamedDecl = Context.Named.Declaration
 
 let discriminate_introduction = ref true
 
-let discr_do_intro () =
-  !discriminate_introduction && Flags.version_strictly_greater Flags.V8_2
+let discr_do_intro () = !discriminate_introduction
 
 open Goptions
 let _ =
   declare_bool_option
-    { optdepr  = false;
+    { optdepr  = true; (* remove in 8.8 *)
       optname  = "automatic introduction of hypotheses by discriminate";
       optkey   = ["Discriminate";"Introduction"];
       optread  = (fun () -> !discriminate_introduction);
@@ -64,13 +63,11 @@ let _ =
 
 let injection_pattern_l2r_order = ref true
 
-let use_injection_pattern_l2r_order () =
-  !injection_pattern_l2r_order
-  && Flags.version_strictly_greater Flags.V8_4
+let use_injection_pattern_l2r_order () = !injection_pattern_l2r_order
 
 let _ =
   declare_bool_option
-    { optdepr  = false;
+    { optdepr  = true; (* remove in 8.8 *)
       optname  = "injection left-to-right pattern order and clear by default when with introduction pattern";
       optkey   = ["Injection";"L2R";"Pattern";"Order"];
       optread  = (fun () -> !injection_pattern_l2r_order) ;
@@ -356,7 +353,6 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
   if (is_global Coqlib.glob_eq hdcncl ||
       (is_global Coqlib.glob_jmeq hdcncl &&
 	 jmeq_same_dom gl ot)) && not dep
-    || Flags.version_less_or_equal Flags.V8_2
   then
     let c = 
       match EConstr.kind sigma hdcncl with 
@@ -1418,7 +1414,7 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
             "" else
             " You can try to use option Set Keep Proof Equalities." in
      tclZEROMSG (strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion))
-  | Inr [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 ->
+  | Inr [([],_,_)] ->
      tclZEROMSG (str"Nothing to inject.")
   | Inr posns ->
       inject_at_positions env sigma l2r u eq_clause posns
@@ -1769,13 +1765,10 @@ type subst_tactic_flags = {
   rewrite_dependent_proof : bool
 }
 
-let default_subst_tactic_flags () =
-  if Flags.version_strictly_greater Flags.V8_2 then
-    { only_leibniz = false; rewrite_dependent_proof = true }
-  else
-    { only_leibniz = true; rewrite_dependent_proof = false }
+let default_subst_tactic_flags =
+  { only_leibniz = false; rewrite_dependent_proof = true }
 
-let subst_all ?(flags=default_subst_tactic_flags ()) () =
+let subst_all ?(flags=default_subst_tactic_flags) () =
 
   if !regular_subst_tactic then
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index d0c6fdca5..689cc48aa 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -63,11 +63,10 @@ let dependent_propositions_elimination = ref true
 
 let use_dependent_propositions_elimination () =
   !dependent_propositions_elimination
-  && Flags.version_strictly_greater Flags.V8_2
 
 let _ =
   declare_bool_option
-    { optdepr  = false;
+    { optdepr  = true; (* remove in 8.8 *)
       optname  = "dependent-propositions-elimination tactic";
       optkey   = ["Dependent";"Propositions";"Elimination"];
       optread  = (fun () -> !dependent_propositions_elimination) ;
@@ -141,11 +140,10 @@ let bracketing_last_or_and_intro_pattern = ref true
 
 let use_bracketing_last_or_and_intro_pattern () =
   !bracketing_last_or_and_intro_pattern
-  && Flags.version_strictly_greater Flags.V8_4
 
 let _ =
   declare_bool_option
-    { optdepr  = false;
+    { optdepr  = true; (* remove in 8.8 *)
       optname  = "bracketing last or-and introduction pattern";
       optkey   = ["Bracketing";"Last";"Introduction";"Pattern"];
       optread  = (fun () -> !bracketing_last_or_and_intro_pattern);
diff --git a/test-suite/bugs/closed/4394.v b/test-suite/bugs/closed/4394.v
deleted file mode 100644
index 1ad81345d..000000000
--- a/test-suite/bugs/closed/4394.v
+++ /dev/null
@@ -1,19 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
-
-Require Import Equality List.
-Inductive Foo (I : Type -> Type) (A : Type) : Type :=
-| foo (B : Type) : A -> I B -> Foo I A.
-Definition Family := Type -> Type.
-Definition FooToo : Family -> Family := Foo.
-Definition optionize (I : Type -> Type) (A : Type) := option (I A).
-Definition bar (I : Type -> Type) (A : Type) : A -> option (I A) -> Foo (optionize I) A := foo (optionize I) A A.
-Record Rec (I : Type -> Type) := { rec : forall A : Type, A -> I A -> Foo I A }.
-Definition barRec : Rec (optionize id) := {| rec := bar id |}.
-Inductive Empty {T} : T -> Prop := .
-Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family) nil)) (b : unit) :
-  Empty (a, b) -> False.
-Proof.
-  intro e.
-  dependent induction e.
-Qed.
-
diff --git a/test-suite/bugs/closed/4400.v b/test-suite/bugs/closed/4400.v
deleted file mode 100644
index a89cf0cbc..000000000
--- a/test-suite/bugs/closed/4400.v
+++ /dev/null
@@ -1,19 +0,0 @@
-(* -*- coq-prog-args: ("-require" "Coq.Compat.Coq84" "-compat" "8.4") -*- *)
-Require Import Coq.Lists.List Coq.Logic.JMeq Program.Equality.
-Set Printing Universes.
-Inductive Foo (I : Type -> Type) (A : Type) : Type :=
-| foo (B : Type) : A -> I B -> Foo I A.
-Definition Family := Type -> Type.
-Definition FooToo : Family -> Family := Foo.
-Definition optionize (I : Type -> Type) (A : Type) := option (I A).
-Definition bar (I : Type -> Type) (A : Type) : A -> option (I A) -> Foo(optionize I) A := foo (optionize I) A A.
-Record Rec (I : Type -> Type) := { rec : forall A : Type, A -> I A -> Foo I A }.
-Definition barRec : Rec (optionize id) := {| rec := bar id |}.
-Inductive Empty {T} : T -> Prop := .
-Theorem empty (family : Family) (a : fold_right prod unit (map (Foo family)
-nil)) (b : unit) :
-  Empty (a, b) -> False.
-Proof.
-  intro e.
-  dependent induction e.
-Qed.
diff --git a/test-suite/bugs/closed/4656.v b/test-suite/bugs/closed/4656.v
deleted file mode 100644
index a59eed2c8..000000000
--- a/test-suite/bugs/closed/4656.v
+++ /dev/null
@@ -1,4 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
-Goal True.
-  constructor 1.
-Qed.
diff --git a/test-suite/bugs/closed/4727.v b/test-suite/bugs/closed/4727.v
deleted file mode 100644
index cfb4548d2..000000000
--- a/test-suite/bugs/closed/4727.v
+++ /dev/null
@@ -1,10 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
-Goal forall (P : Set) (l : P) (P0 : Set) (w w0 : P0) (T : Type) (a : P * T) (o : P -> option P0),
-    (forall (l1 l2 : P) (w1 : P0), o l1 = Some w1 -> o l2 = Some w1 -> l1 = l2) ->
-    o l = Some w -> o (fst a) = Some w0 -> {w = w0} + {w <> w0} -> False.
-Proof.
-  clear; intros ???????? inj H0 H1 H2.
-  destruct H2; intuition subst.
-  eapply inj in H1; [ | eauto ].
-  progress subst. (* should succeed, used to not succeed *)
-Abort.
diff --git a/test-suite/bugs/closed/4733.v b/test-suite/bugs/closed/4733.v
deleted file mode 100644
index a90abd71c..000000000
--- a/test-suite/bugs/closed/4733.v
+++ /dev/null
@@ -1,52 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
-(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5.  If they use*)
-Require Import Coq.Lists.List.
-Require Import Coq.Vectors.Vector.
-Import ListNotations.
-Import VectorNotations.
-Set Implicit Arguments.
-Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T).
-Arguments mynil {_}, _.
-
-Delimit Scope mylist_scope with mylist.
-Bind Scope mylist_scope with mylist.
-Delimit Scope vector_scope with vector.
-
-Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
-Notation " [ x ] " := (mycons x mynil) : mylist_scope.
-Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope.
-
-(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4.  There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *)
-Check [ ]%mylist : mylist _.
-Check [ ]%list : list _.
-Check []%vector : Vector.t _ _.
-Check [ _ ]%mylist : mylist _.
-Check [ _ ]%list : list _.
-Check [ _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%list : list _.
-Check [ _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ; _ ]%mylist : mylist _.
-
-Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z mynil) ..)) : mylist_scope.
-(* Now these all work, but not so in 8.4.  If we get the ability to remove notations, this section can also just be removed. *)
-Check [ ]%mylist : mylist _.
-Check [ ]%list : list _.
-Check []%vector : Vector.t _ _.
-Check [ _ ]%mylist : mylist _.
-Check [ _ ]%list : list _.
-Check [ _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%list : list _.
-Check [ _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ; _ ]%mylist : mylist _.
diff --git a/test-suite/bugs/opened/4803.v b/test-suite/bugs/opened/4803.v
deleted file mode 100644
index 4541f13d0..000000000
--- a/test-suite/bugs/opened/4803.v
+++ /dev/null
@@ -1,48 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
-(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5.  If they use*)
-Require Import Coq.Lists.List.
-Require Import Coq.Vectors.Vector.
-Import ListNotations.
-Import VectorNotations.
-Set Implicit Arguments.
-Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T).
-Arguments mynil {_}, _.
-
-Delimit Scope mylist_scope with mylist.
-Bind Scope mylist_scope with mylist.
-Delimit Scope vector_scope with vector.
-
-Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
-Notation " [ x ] " := (mycons x mynil) : mylist_scope.
-Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope.
-
-(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4.  There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *)
-Check [ ]%mylist : mylist _.
-Check [ ]%list : list _.
-Check []%vector : Vector.t _ _.
-Check [ _ ]%mylist : mylist _.
-Check [ _ ]%list : list _.
-Check [ _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%list : list _.
-Check [ _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ]%mylist : mylist _.
-Check [ _ ; _ ; _ ; _ ]%list : list _.
-Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _.
-Check [ _ ; _ ; _ ; _ ]%mylist : mylist _.
-
-(** Now check that we can add and then remove notations from the parser *)
-(* We should be able to stick some vernacular here to remove [] from the parser *)
-Fail Remove Notation "[]".
-Goal True.
-  (* This should not be a syntax error; before moving this file to closed, uncomment this line. *)
-  (* idtac; []. *)
-  constructor.
-Qed.
-
-Check { _ : _ & _ }.
-Reserved Infix "&" (at level 0).
-Fail Remove Infix "&".
-(* Check { _ : _ & _ }. *)
diff --git a/test-suite/success/Compat84.v b/test-suite/success/Compat84.v
deleted file mode 100644
index 732a024fc..000000000
--- a/test-suite/success/Compat84.v
+++ /dev/null
@@ -1,19 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.4") -*- *)
-
-Goal True.
-  solve [ constructor 1 ]. Undo.
-  solve [ econstructor 1 ]. Undo.
-  solve [ constructor ]. Undo.
-  solve [ econstructor ]. Undo.
-  solve [ constructor (fail) ]. Undo.
-  solve [ econstructor (fail) ]. Undo.
-  split.
-Qed.
-
-Goal False \/ True.
-  solve [ constructor (constructor) ]. Undo.
-  solve [ econstructor (econstructor) ]. Undo.
-  solve [ constructor 2; constructor ]. Undo.
-  solve [ econstructor 2; econstructor ]. Undo.
-  right; esplit.
-Qed.
diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v
index 3d7ef01fb..cfe0e08ed 100644
--- a/theories/Classes/CRelationClasses.v
+++ b/theories/Classes/CRelationClasses.v
@@ -305,9 +305,7 @@ Section Binary.
     fun x y => sum (R x y) (R' x y).
   
   (** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
-  
-  Set Automatic Introduction.
-  
+
   Global Instance relation_equivalence_equivalence :
     Equivalence relation_equivalence.
   Proof. split; red; unfold relation_equivalence, iffT. firstorder. 
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 11c204dae..57728d305 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -433,9 +433,7 @@ Section Binary.
     @predicate_union (A::A::Tnil) R R'.
   
   (** Relation equivalence is an equivalence, and subrelation defines a partial order. *)
-  
-  Set Automatic Introduction.
-  
+
   Global Instance relation_equivalence_equivalence :
     Equivalence relation_equivalence.
   Proof. exact (@predicate_equivalence_equivalence (A::A::Tnil)). Qed.
diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v
deleted file mode 100644
index a3e23f91c..000000000
--- a/theories/Compat/Coq84.v
+++ /dev/null
@@ -1,79 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(** Compatibility file for making Coq act similar to Coq v8.4 *)
-
-(** Any compatibility changes to make future versions of Coq behave like Coq 8.5 are likely needed to make them behave like Coq 8.4. *)
-Require Export Coq.Compat.Coq85.
-
-(** See https://coq.inria.fr/bugs/show_bug.cgi?id=4319 for updates *)
-(** This is required in Coq 8.5 to use the [omega] tactic; in Coq 8.4, it's automatically available.  But ZArith_base puts infix ~ at level 7, and we don't want that, so we don't [Import] it. *)
-Require Coq.omega.Omega.
-Ltac omega := Coq.omega.Omega.omega.
-
-(** The number of arguments given in [match] statements has changed from 8.4 to 8.5. *)
-Global Set Asymmetric Patterns.
-
-(** The automatic elimination schemes for records were dropped by default in 8.5.  This restores the default behavior of Coq 8.4. *)
-Global Set Nonrecursive Elimination Schemes.
-
-(** See bug 3545 *)
-Global Set Universal Lemma Under Conjunction.
-
-(** Feature introduced in 8.5, disabled by default and configurable since 8.6. *)
-Global Unset Refolding Reduction.
-
-(** In 8.4, [constructor (tac)] allowed backtracking across the use of [constructor]; it has been subsumed by [constructor; tac]. *)
-Ltac constructor_84_n n := constructor n.
-Ltac constructor_84_tac tac := once (constructor; tac).
-
-Tactic Notation "constructor" := Coq.Init.Notations.constructor.
-Tactic Notation "constructor" int_or_var(n) := constructor_84_n n.
-Tactic Notation "constructor" "(" tactic(tac) ")" := constructor_84_tac tac.
-
-(** In 8.4, [econstructor (tac)] allowed backtracking across the use of [econstructor]; it has been subsumed by [econstructor; tac]. *)
-Ltac econstructor_84_n n := econstructor n.
-Ltac econstructor_84_tac tac := once (econstructor; tac).
-
-Tactic Notation "econstructor" := Coq.Init.Notations.econstructor.
-Tactic Notation "econstructor" int_or_var(n) := econstructor_84_n n.
-Tactic Notation "econstructor" "(" tactic(tac) ")" := econstructor_84_tac tac.
-
-(** Some tactic notations do not factor well with tactics; we add global parsing entries for some tactics that would otherwise be overwritten by custom variants. See https://coq.inria.fr/bugs/show_bug.cgi?id=4392. *)
-Tactic Notation "reflexivity" := reflexivity.
-Tactic Notation "assumption" := assumption.
-Tactic Notation "etransitivity" := etransitivity.
-Tactic Notation "cut" constr(c) := cut c.
-Tactic Notation "exact_no_check" constr(c) := exact_no_check c.
-Tactic Notation "vm_cast_no_check" constr(c) := vm_cast_no_check c.
-Tactic Notation "casetype" constr(c) := casetype c.
-Tactic Notation "elimtype" constr(c) := elimtype c.
-Tactic Notation "lapply" constr(c) := lapply c.
-Tactic Notation "transitivity" constr(c) := transitivity c.
-Tactic Notation "left" := left.
-Tactic Notation "eleft" := eleft.
-Tactic Notation "right" := right.
-Tactic Notation "eright" := eright.
-Tactic Notation "symmetry" := symmetry.
-Tactic Notation "split" := split.
-Tactic Notation "esplit" := esplit.
-
-(** Many things now import [PeanoNat] rather than [NPeano], so we require it so that the old absolute names in [NPeano.Nat] are available. *)
-Require Coq.Numbers.Natural.Peano.NPeano.
-
-(** The following coercions were declared by default in Specif.v. *)
-Coercion sig_of_sig2 : sig2 >-> sig.
-Coercion sigT_of_sigT2 : sigT2 >-> sigT.
-Coercion sigT_of_sig : sig >-> sigT.
-Coercion sig_of_sigT : sigT >-> sig.
-Coercion sigT2_of_sig2 : sig2 >-> sigT2.
-Coercion sig2_of_sigT2 : sigT2 >-> sig2.
-
-(** In 8.4, the statement of admitted lemmas did not depend on the section
-    variables. *)
-Unset Keep Admitted Variables.
diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v
index 3697999f7..6a5233b64 100644
--- a/theories/Reals/SeqProp.v
+++ b/theories/Reals/SeqProp.v
@@ -150,7 +150,7 @@ Definition sequence_lb (Un:nat -> R) (pr:has_lb Un)
 (* Compatibility *)
 Notation sequence_majorant := sequence_ub (only parsing).
 Notation sequence_minorant := sequence_lb (only parsing).
-Unset Standard Proposition Elimination Names.
+
 Lemma Wn_decreasing :
   forall (Un:nat -> R) (pr:has_ub Un), Un_decreasing (sequence_ub Un pr).
 Proof.
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 16fe40555..f36d0c348 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -126,14 +126,12 @@ let init_ocaml_path () =
     Mltop.add_ml_dir (Envars.coqlib ());
     List.iter add_subdir Coq_config.all_src_dirs
 
-let get_compat_version = function
+let get_compat_version ?(allow_old = true) = function
   | "8.7" -> Flags.Current
   | "8.6" -> Flags.V8_6
   | "8.5" -> Flags.V8_5
-  | "8.4" -> Flags.V8_4
-  | "8.3" -> Flags.V8_3
-  | "8.2" -> Flags.V8_2
-  | ("8.1" | "8.0") as s ->
+  | ("8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
+    if allow_old then Flags.VOld else
     CErrors.user_err ~hdr:"get_compat_version"
       (str "Compatibility with version " ++ str s ++ str " not supported.")
   | s -> CErrors.user_err ~hdr:"get_compat_version"
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 3b42289ee..787dfb61a 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -25,4 +25,4 @@ val init_library_roots : unit -> unit
 
 val init_ocaml_path : unit -> unit
 
-val get_compat_version : string -> Flags.compat_version
+val get_compat_version : ?allow_old:bool -> string -> Flags.compat_version
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 31450ebd5..5f0716fd9 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -205,9 +205,9 @@ let require () =
 
 let add_compat_require v =
   match v with
-  | Flags.V8_4 -> add_require "Coq.Compat.Coq84"
   | Flags.V8_5 -> add_require "Coq.Compat.Coq85"
-  | _ -> ()
+  | Flags.V8_6 -> add_require "Coq.Compat.Coq86"
+  | Flags.VOld | Flags.Current -> ()
 
 let compile_list = ref ([] : (bool * string) list)
 
@@ -514,7 +514,9 @@ let parse_args arglist =
     |"-async-proofs-delegation-threshold" ->
         Flags.async_proofs_delegation_threshold:= get_float opt (next ())
     |"-worker-id" -> set_worker_id opt (next ())
-    |"-compat" -> let v = get_compat_version (next ()) in Flags.compat_version := v; add_compat_require v
+    |"-compat" ->
+        let v = get_compat_version ~allow_old:false (next ()) in
+        Flags.compat_version := v; add_compat_require v
     |"-compile" -> add_compile false (next ())
     |"-compile-verbose" -> add_compile true (next ())
     |"-dump-glob" -> Dumpglob.dump_into_file (next ()); glob_opt := true
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index c2c27eb78..44d6f37cc 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -84,15 +84,8 @@ let _ =
       optkey   = ["Boolean";"Equality";"Schemes"];
       optread  = (fun () -> !eq_flag) ;
       optwrite = (fun b -> eq_flag := b) }
-let _ = (* compatibility *)
-  declare_bool_option
-    { optdepr  = true;
-      optname  = "automatic declaration of boolean equality";
-      optkey   = ["Equality";"Scheme"];
-      optread  = (fun () -> !eq_flag) ;
-      optwrite = (fun b -> eq_flag := b) }
 
-let is_eq_flag () = !eq_flag && Flags.version_strictly_greater Flags.V8_2
+let is_eq_flag () = !eq_flag
 
 let eq_dec_flag = ref false 
 let _ =
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index c76ced56f..6714b98f5 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1287,7 +1287,7 @@ let _ =
 
 let _ =
   declare_bool_option
-    { optdepr  = false;
+    { optdepr  = true; (* remove in 8.8 *)
       optname  = "automatic introduction of variables";
       optkey   = ["Automatic";"Introduction"];
       optread  = Flags.is_auto_intros;
@@ -1383,17 +1383,6 @@ let _ =
       optread  = (fun () -> !CClosure.share);
       optwrite = (fun b -> CClosure.share := b) }
 
-(* No more undo limit in the new proof engine.
-   The command still exists for compatibility (e.g. with ProofGeneral) *)
-
-let _ =
-  declare_int_option
-    { optdepr  = true;
-      optname  = "the undo limit (OBSOLETE)";
-      optkey   = ["Undo"];
-      optread  = (fun _ -> None);
-      optwrite = (fun _ -> ()) }
-
 let _ =
   declare_bool_option
     { optdepr  = false;