Remove VOld compatibility flag.

10 files changed, 7 insertions, 61 deletions

diff --git a/lib/flags.ml b/lib/flags.ml
index 5da131020..ac8e4ce47 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -67,14 +67,11 @@ 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_5 | V8_6 | V8_7 | Current
+type compat_version = V8_5 | V8_6 | V8_7 | Current
 
 let compat_version = ref Current
 
 let version_compare v1 v2 = match v1, v2 with
-  | VOld, VOld -> 0
-  | VOld, _ -> -1
-  | _, VOld -> 1
   | V8_5, V8_5 -> 0
   | V8_5, _ -> -1
   | _, V8_5 -> 1
@@ -90,7 +87,6 @@ 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
-  | VOld -> "old"
   | V8_5 -> "8.5"
   | V8_6 -> "8.6"
   | V8_7 -> "8.7"
diff --git a/lib/flags.mli b/lib/flags.mli
index bc07dec80..c85055783 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -43,7 +43,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_5 | V8_6 | V8_7 | Current
+type compat_version = V8_5 | V8_6 | V8_7 | 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/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 93e534e0b..6193ceb1a 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -58,7 +58,6 @@ let parse_compat_version ?(allow_old = true) = let open Flags in function
   | "8.6" -> V8_6
   | "8.5" -> V8_5
   | ("8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s ->
-    if allow_old then VOld else
     CErrors.user_err ~hdr:"get_compat_version"
       Pp.(str "Compatibility with version " ++ str s ++ str " not supported.")
   | s ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 6700748eb..bfc04893d 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -923,7 +923,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	  | [], [] -> []
 	  | _ -> assert false
 	in aux 1 1 (List.rev nal) cs.cs_args, true in
-    let fsign = if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld
+    let fsign = if Flags.version_strictly_greater Flags.V8_6
                 then Context.Rel.map (whd_betaiota !evdref) fsign
                 else fsign (* beta-iota-normalization regression in 8.5 and 8.6 *) in
     let obj ind p v f =
@@ -1036,7 +1036,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
 	let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in
         let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in
         let cs_args =
-          if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld
+          if Flags.version_strictly_greater Flags.V8_6
           then Context.Rel.map (whd_betaiota !evdref) cs_args
           else cs_args (* beta-iota-normalization regression in 8.5 and 8.6 *) in
 	let csgn =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e1720ec95..48d8a372c 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -193,7 +193,7 @@ let pose_all_metas_as_evars env evd t =
         let ty = EConstr.of_constr ty in
         let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in
         let ty =
-          if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld
+          if Flags.version_strictly_greater Flags.V8_6
           then nf_betaiota env evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *)
           else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in
         let src = Evd.evar_source_of_meta mv !evdref in
diff --git a/test-suite/bugs/closed/4785_compat_85.v b/test-suite/bugs/closed/4785_compat_85.v
deleted file mode 100644
index bbb34f465..000000000
--- a/test-suite/bugs/closed/4785_compat_85.v
+++ /dev/null
@@ -1,46 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.5") -*- *)
-Require Coq.Lists.List Coq.Vectors.Vector.
-Require Coq.Compat.Coq85.
-
-Module A.
-Import Coq.Lists.List Coq.Vectors.Vector.
-Import ListNotations.
-Check [ ]%list : list _.
-Import VectorNotations ListNotations.
-Delimit Scope vector_scope with vector.
-Check [ ]%vector : Vector.t _ _.
-Check []%vector : Vector.t _ _.
-Check [ ]%list : list _.
-Fail Check []%list : list _.
-
-Goal True.
-  idtac; [ ]. (* Note that vector notations break the [ | .. | ] syntax of Ltac *)
-Abort.
-
-Inductive mylist A := mynil | mycons (x : A) (xs : mylist A).
-Delimit Scope mylist_scope with mylist.
-Bind Scope mylist_scope with mylist.
-Arguments mynil {_}, _.
-Arguments mycons {_} _ _.
-Notation " [] " := mynil (compat "8.5") : mylist_scope.
-Notation " [ ] " := mynil (format "[ ]") : mylist_scope.
-Notation " [ x ] " := (mycons x nil) : mylist_scope.
-Notation " [ x ; y ; .. ; z ] " :=  (mycons x (mycons y .. (mycons z nil) ..)) : mylist_scope.
-
-Import Coq.Compat.Coq85.
-Locate Module VectorNotations.
-Import VectorDef.VectorNotations.
-
-Check []%vector : Vector.t _ _.
-Check []%mylist : mylist _.
-Check [ ]%mylist : mylist _.
-Check [ ]%list : list _.
-End A.
-
-Module B.
-Import Coq.Compat.Coq85.
-
-Goal True.
-  idtac; []. (* Check that importing the compat file doesn't break the [ | .. | ] syntax of Ltac *)
-Abort.
-End B.
diff --git a/test-suite/bugs/closed/4798.v b/test-suite/bugs/closed/4798.v
index dbc3d46fc..6f2bcb968 100644
--- a/test-suite/bugs/closed/4798.v
+++ b/test-suite/bugs/closed/4798.v
@@ -1,3 +1,3 @@
 Check match 2 with 0 => 0 | S n => n end.
-Notation "|" := 1 (compat "8.4").
+Notation "|" := 1 (compat "8.6").
 Check match 2 with 0 => 0 | S n => n end. (* fails *)
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index eae2c52de..301528598 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -27,7 +27,6 @@ Module ListNotations.
 Notation "[ ]" := nil (format "[ ]") : list_scope.
 Notation "[ x ]" := (cons x nil) : list_scope.
 Notation "[ x ; y ; .. ; z ]" :=  (cons x (cons y .. (cons z nil) ..)) : list_scope.
-Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..) (compat "8.4") : list_scope.
 End ListNotations.
 
 Import ListNotations.
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index c49451776..a21b9ca98 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -305,12 +305,10 @@ End VECTORLIST.
 Module VectorNotations.
 Delimit Scope vector_scope with vector.
 Notation "[ ]" := [] (format "[ ]") : vector_scope.
-Notation "[]" := [] (compat "8.5") : vector_scope.
 Notation "h :: t" := (h :: t) (at level 60, right associativity)
   : vector_scope.
 Notation "[ x ]" := (x :: []) : vector_scope.
 Notation "[ x ; y ; .. ; z ]" := (cons _ x _ (cons _ y _ .. (cons _ z _ (nil _)) ..)) : vector_scope.
-Notation "[ x ; .. ; y ]" := (cons _ x _ .. (cons _ y _ (nil _)) ..) (compat "8.4") : vector_scope.
 Notation "v [@ p ]" := (nth v p) (at level 1, format "v [@ p ]") : vector_scope.
 Open Scope vector_scope.
 End VectorNotations.
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index a7065c031..46db9a390 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -149,7 +149,7 @@ let add_compat_require opts v =
   | Flags.V8_5 -> add_vo_require opts "Coq.Compat.Coq85" None (Some false)
   | Flags.V8_6 -> add_vo_require opts "Coq.Compat.Coq86" None (Some false)
   | Flags.V8_7 -> add_vo_require opts "Coq.Compat.Coq87" None (Some false)
-  | Flags.VOld | Flags.Current -> opts
+  | Flags.Current -> opts
 
 let set_batch_mode opts =
   Flags.quiet := true;