Remove support for Coq 8.2.

10 files changed, 13 insertions, 29 deletions

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 682e2e4df..c4a97bd12 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -106,7 +106,7 @@ 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 = VOld | V8_2 | V8_3 | V8_4 | V8_5 | V8_6 | Current
+type compat_version = VOld | V8_3 | V8_4 | V8_5 | V8_6 | Current
 
 let compat_version = ref Current
 
@@ -114,9 +114,6 @@ let version_compare v1 v2 = match v1, v2 with
   | VOld, VOld -> 0
   | VOld, _ -> -1
   | _, VOld -> 1
-  | V8_2, V8_2 -> 0
-  | V8_2, _ -> -1
-  | _, V8_2 -> 1
   | V8_3, V8_3 -> 0
   | V8_3, _ -> -1
   | _, V8_3 -> 1
@@ -136,7 +133,6 @@ let version_less_or_equal v = not (version_strictly_greater v)
 
 let pr_version = function
   | VOld -> "old"
-  | V8_2 -> "8.2"
   | V8_3 -> "8.3"
   | V8_4 -> "8.4"
   | V8_5 -> "8.5"
@@ -161,7 +157,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 c0aca9c99..6e9362681 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 = VOld | V8_2 | V8_3 | V8_4 | V8_5 | V8_6 | Current
+type compat_version = VOld | V8_3 | V8_4 | 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..c6cc955b0 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 _ =
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 9a973cff5..627a9c9cc 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -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..3e0eb9d91 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -481,7 +481,6 @@ 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
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 05c5cd5ec..46c042b8b 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -50,8 +50,7 @@ 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 _ =
@@ -356,7 +355,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 
@@ -1769,13 +1767,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 b553f316c..ebfaab5bf 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -64,7 +64,6 @@ 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
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 33b032704..af0c18fa2 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -132,8 +132,7 @@ let get_compat_version ?(allow_old = true) = function
   | "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.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.")
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index c2c27eb78..e90c25926 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -92,7 +92,7 @@ let _ = (* compatibility *)
       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 _ =