From 571c319ed536cb2757176d3ae4007a75f5d3b04d Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Nov 2016 17:08:14 +0100 Subject: Remove support for Coq 8.2. --- pretyping/classops.ml | 8 ++------ pretyping/unification.ml | 1 - 2 files changed, 2 insertions(+), 7 deletions(-) (limited to 'pretyping') diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 9a973cff55..627a9c9cc7 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 0fb48ed8cf..3e0eb9d91b 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 -- cgit v1.2.3 From daf5335b18c926d7130cd28e50f00cc49c4011f6 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Nov 2016 17:12:58 +0100 Subject: Remove support for Coq 8.3. --- pretyping/unification.ml | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) (limited to 'pretyping') diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 3e0eb9d91b..ef4f7f7545 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 -- cgit v1.2.3 From 376da97be60957b25e59afb5791fae665127b17b Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Nov 2016 17:48:14 +0100 Subject: Remove options deprecated since 8.4. --- pretyping/unification.ml | 13 +------------ 1 file changed, 1 insertion(+), 12 deletions(-) (limited to 'pretyping') diff --git a/pretyping/unification.ml b/pretyping/unification.ml index ef4f7f7545..b4964c1f36 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -248,20 +248,9 @@ let sort_eqns = unify_r2l let global_pattern_unification_flag = ref true -(* Compatibility option introduced and activated in Coq 8.3 whose - syntax is now deprecated. *) - open Goptions -let _ = - declare_bool_option - { optdepr = true; - optname = "pattern-unification for existential variables in tactics"; - optkey = ["Tactic";"Evars";"Pattern";"Unification"]; - optread = (fun () -> !global_pattern_unification_flag); - optwrite = (:=) global_pattern_unification_flag } -(* Compatibility option superseding the previous one, introduced and - activated in Coq 8.4 *) +(* Compatibility option introduced and activated in Coq 8.4 *) let _ = declare_bool_option -- cgit v1.2.3 From 5e93f1e95853c3614df813845b94051a45f1a749 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Nov 2016 17:51:32 +0100 Subject: Deprecate options that were introduced for compatibility with 8.2. --- pretyping/classops.ml | 2 +- pretyping/unification.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping') diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 627a9c9cc7..8d87f6e99c 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -428,7 +428,7 @@ let automatically_import_coercions = ref false open Goptions let _ = declare_bool_option - { optdepr = false; + { optdepr = true; (* remove in 8.8 *) optname = "automatic import of coercions"; optkey = ["Automatic";"Coercions";"Import"]; optread = (fun () -> !automatically_import_coercions); diff --git a/pretyping/unification.ml b/pretyping/unification.ml index b4964c1f36..67c8b07e78 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -254,7 +254,7 @@ open Goptions let _ = declare_bool_option - { optdepr = false; + { optdepr = true; (* remove in 8.8 *) optname = "pattern-unification for existential variables in tactics"; optkey = ["Tactic";"Pattern";"Unification"]; optread = (fun () -> !global_pattern_unification_flag); -- cgit v1.2.3