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. --- toplevel/coqargs.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'toplevel') 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 From 3ce123f16ce19f67dde4a0f3f2874a2678649907 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 20 Feb 2018 16:03:57 +0100 Subject: Remove 8.5 compatibility support. --- doc/stdlib/index-list.html.template | 1 - lib/flags.ml | 6 +----- lib/flags.mli | 2 +- parsing/g_vernac.ml4 | 3 +-- pretyping/unification.ml | 7 +------ tactics/contradiction.ml | 6 +----- tactics/equality.ml | 2 +- tactics/tactics.ml | 8 +------- test-suite/bugs/closed/4785.v | 11 ----------- test-suite/bugs/closed/4873.v | 1 - theories/Compat/Coq85.v | 36 ------------------------------------ toplevel/coqargs.ml | 1 - 12 files changed, 7 insertions(+), 77 deletions(-) delete mode 100644 theories/Compat/Coq85.v (limited to 'toplevel') diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 95e541f81..a2739e457 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -596,7 +596,6 @@ through the Require Import command.

theories/Compat/AdmitAxiom.v - theories/Compat/Coq85.v theories/Compat/Coq86.v theories/Compat/Coq87.v
diff --git a/lib/flags.ml b/lib/flags.ml index ac8e4ce47..12ed2a450 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 = V8_5 | V8_6 | V8_7 | Current +type compat_version = V8_6 | V8_7 | Current let compat_version = ref Current let version_compare v1 v2 = match v1, v2 with - | V8_5, V8_5 -> 0 - | V8_5, _ -> -1 - | _, V8_5 -> 1 | V8_6, V8_6 -> 0 | V8_6, _ -> -1 | _, V8_6 -> 1 @@ -87,7 +84,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 - | V8_5 -> "8.5" | V8_6 -> "8.6" | V8_7 -> "8.7" | Current -> "current" diff --git a/lib/flags.mli b/lib/flags.mli index c85055783..148b2ca5e 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 = V8_5 | V8_6 | V8_7 | Current +type compat_version = 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 6193ceb1a..4d6741ff5 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -56,8 +56,7 @@ let parse_compat_version ?(allow_old = true) = let open Flags in function | "8.8" -> Current | "8.7" -> V8_7 | "8.6" -> V8_6 - | "8.5" -> V8_5 - | ("8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> + | ("8.5" | "8.4" | "8.3" | "8.2" | "8.1" | "8.0") as s -> CErrors.user_err ~hdr:"get_compat_version" Pp.(str "Compatibility with version " ++ str s ++ str " not supported.") | s -> diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 48d8a372c..6106b6ef6 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1304,12 +1304,7 @@ let solve_simple_evar_eqn ts env evd ev rhs = match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) with | UnifFailure (evd,reason) -> error_cannot_unify env evd ~reason (mkEvar ev,rhs); - | Success evd -> - if Flags.version_less_or_equal Flags.V8_5 then - (* We used to force solving unrelated problems at arbitrary times *) - Evarconv.solve_unif_constraints_with_heuristics env evd - else (* solve_simple_eqn calls reconsider_unif_constraints itself *) - evd + | Success evd -> evd (* [w_merge env sigma b metas evars] merges common instances in metas or in evars, possibly generating new unification problems; if [b] diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 467754a84..3386f972e 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -44,8 +44,6 @@ let absurd c = absurd c (* Contradiction *) -let use_negated_unit_or_eq_type () = Flags.version_strictly_greater Flags.V8_5 - (** [f] does not assume its argument to be [nf_evar]-ed. *) let filter_hyp f tac = let rec seek = function @@ -71,9 +69,7 @@ let contradiction_context = simplest_elim (mkVar id) else match EConstr.kind sigma typ with | Prod (na,t,u) when is_empty_type sigma u -> - let is_unit_or_eq = - if use_negated_unit_or_eq_type () then match_with_unit_or_eq_type sigma t - else None in + let is_unit_or_eq = match_with_unit_or_eq_type sigma t in Tacticals.New.tclORELSE (match is_unit_or_eq with | Some _ -> diff --git a/tactics/equality.ml b/tactics/equality.ml index 9a1ac768c..0ce7fa022 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -84,7 +84,7 @@ let _ = let injection_in_context = ref false let use_injection_in_context = function - | None -> !injection_in_context && Flags.version_strictly_greater Flags.V8_5 + | None -> !injection_in_context | Some flags -> flags.injection_in_context let _ = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 7e281e2fe..bf9271ba9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5146,16 +5146,10 @@ module New = struct open Locus let reduce_after_refine = - let onhyps = - (** We reduced everywhere in the hyps before 8.6 *) - if Flags.version_compare !Flags.compat_version Flags.V8_5 == 0 - then None - else Some [] - in reduce (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true; rZeta=false;rDelta=false;rConst=[]}) - {onhyps; concl_occs=AllOccurrences } + {onhyps = Some []; concl_occs = AllOccurrences } let refine ~typecheck c = Refine.refine ~typecheck c <*> diff --git a/test-suite/bugs/closed/4785.v b/test-suite/bugs/closed/4785.v index c3c97d3f5..0d347b262 100644 --- a/test-suite/bugs/closed/4785.v +++ b/test-suite/bugs/closed/4785.v @@ -1,5 +1,4 @@ Require Coq.Lists.List Coq.Vectors.Vector. -Require Coq.Compat.Coq85. Module A. Import Coq.Lists.List Coq.Vectors.Vector. @@ -21,12 +20,10 @@ 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. @@ -35,11 +32,3 @@ 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/4873.v b/test-suite/bugs/closed/4873.v index 3be36d847..39299883a 100644 --- a/test-suite/bugs/closed/4873.v +++ b/test-suite/bugs/closed/4873.v @@ -1,6 +1,5 @@ Require Import Coq.Classes.Morphisms. Require Import Relation_Definitions. -Require Import Coq.Compat.Coq85. Fixpoint tuple' T n : Type := match n with diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v deleted file mode 100644 index 56a9130d1..000000000 --- a/theories/Compat/Coq85.v +++ /dev/null @@ -1,36 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* C", does not - behave as "intros [H|H]" but leave instead hypotheses quantified in - the goal, here producing subgoals A->C and B->C. *) - -Global Unset Bracketing Last Introduction Pattern. -Global Unset Regular Subst Tactic. -Global Unset Structural Injection. -Global Unset Shrink Abstract. -Global Unset Shrink Obligations. -Global Set Refolding Reduction. - -(** The resolution algorithm for type classes has changed. *) -Global Set Typeclasses Legacy Resolution. -Global Set Typeclasses Limit Intros. -Global Unset Typeclasses Filtered Unification. - -(** Allow silently letting unification constraints float after a "." *) -Global Unset Solve Unification Constraints. diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 46db9a390..673cfdb99 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -146,7 +146,6 @@ let add_vo_require opts d p export = let add_compat_require opts v = match v with - | 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.Current -> opts -- cgit v1.2.3