From a4817d25befc71b7dbf707637660431144985133 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 20 Feb 2018 13:55:46 +0100 Subject: Remove VOld compatibility flag. --- lib/flags.ml | 6 +---- lib/flags.mli | 2 +- parsing/g_vernac.ml4 | 1 - pretyping/pretyping.ml | 4 +-- pretyping/unification.ml | 2 +- test-suite/bugs/closed/4785_compat_85.v | 46 --------------------------------- test-suite/bugs/closed/4798.v | 2 +- theories/Lists/List.v | 1 - theories/Vectors/VectorDef.v | 2 -- toplevel/coqargs.ml | 2 +- 10 files changed, 7 insertions(+), 61 deletions(-) delete mode 100644 test-suite/bugs/closed/4785_compat_85.v 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; -- cgit v1.2.3