Remove support for Coq 8.3.

5 files changed, 6 insertions, 15 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index c4a97bd12..d738e3df1 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_3 | V8_4 | V8_5 | V8_6 | Current
+type compat_version = VOld | 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_3, V8_3 -> 0
-  | V8_3, _ -> -1
-  | _, V8_3 -> 1
   | V8_4, V8_4 -> 0
   | V8_4, _ -> -1
   | _, V8_4 -> 1
@@ -133,7 +130,6 @@ let version_less_or_equal v = not (version_strictly_greater v)
 
 let pr_version = function
   | VOld -> "old"
-  | V8_3 -> "8.3"
   | V8_4 -> "8.4"
   | V8_5 -> "8.5"
   | V8_6 -> "8.6"
diff --git a/lib/flags.mli b/lib/flags.mli
index 6e9362681..d6a0eac44 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_3 | V8_4 | V8_5 | V8_6 | Current
+type compat_version = VOld | 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/pretyping/unification.ml b/pretyping/unification.ml
index 3e0eb9d91..ef4f7f754 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -484,8 +484,7 @@ let use_evars_pattern_unification flags =
 
 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 = 
@@ -608,9 +607,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
@@ -948,7 +944,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 46c042b8b..5c2370253 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1416,7 +1416,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
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index af0c18fa2..4a17a5ee1 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -131,8 +131,7 @@ let get_compat_version ?(allow_old = true) = function
   | "8.6" -> Flags.V8_6
   | "8.5" -> Flags.V8_5
   | "8.4" -> Flags.V8_4
-  | "8.3" -> Flags.V8_3
-  | ("8.2" | "8.1" | "8.0") as s ->
+  | ("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.")