From 7146036f5a4555840a75b1fb564ee3c1b54623dc Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 11 May 2017 13:38:47 -0400 Subject: s/appcontext/context/ They mean the same thing since 8.5, and appcontext is deprecated. --- Makefile | 4 ++-- src/Compilers/EtaWf.v | 2 +- src/Compilers/ExprInversion.v | 8 ++++---- src/Compilers/Reify.v | 2 +- src/Compilers/Z/OpInversion.v | 4 ++-- src/LegacyArithmetic/Pow2BaseProofs.v | 6 +++--- src/Util/ListUtil.v | 12 ++++++------ src/Util/Tactics/BreakMatch.v | 20 ++++++++++---------- src/Util/Tactics/Contains.v | 4 ++-- src/Util/Tactics/Revert.v | 4 ++-- src/Util/Tactics/SetEvars.v | 2 +- src/Util/Tactics/SimplifyProjections.v | 2 +- src/Util/WordUtil.v | 2 +- src/Util/ZUtil.v | 8 ++++---- 14 files changed, 40 insertions(+), 40 deletions(-) diff --git a/Makefile b/Makefile index 3324ec86a..1d4020efb 100644 --- a/Makefile +++ b/Makefile @@ -76,9 +76,9 @@ COQPRIME_FOLDER := coqprime ifneq ($(filter 8.5%,$(COQ_VERSION)),) # 8.5 else ifneq ($(PROFILE),) -OTHERFLAGS ?= -profile-ltac -w "-deprecated-appcontext -notation-overridden" +OTHERFLAGS ?= -profile-ltac -w "-notation-overridden" else -OTHERFLAGS ?= -w "-deprecated-appcontext -notation-overridden" +OTHERFLAGS ?= -w "-notation-overridden" endif endif diff --git a/src/Compilers/EtaWf.v b/src/Compilers/EtaWf.v index e8dd2f846..1134b5d05 100644 --- a/src/Compilers/EtaWf.v +++ b/src/Compilers/EtaWf.v @@ -28,7 +28,7 @@ Section language. | _ => progress split_iff | _ => rewrite eq_interp_flat_type_eta_gen by assumption | [ H : _ |- _ ] => rewrite eq_interp_flat_type_eta_gen in H by assumption - | [ H : appcontext[interp_flat_type_eta_gen] |- _ ] + | [ H : context[interp_flat_type_eta_gen] |- _ ] => setoid_rewrite eq_interp_flat_type_eta_gen in H; [ | assumption.. ] | _ => progress break_match | [ H : wff _ _ _ |- _ ] => solve [ inversion H ] diff --git a/src/Compilers/ExprInversion.v b/src/Compilers/ExprInversion.v index a1d2587f5..48ea30907 100644 --- a/src/Compilers/ExprInversion.v +++ b/src/Compilers/ExprInversion.v @@ -174,13 +174,13 @@ Ltac invert_expr := repeat invert_expr_step. Ltac invert_match_expr_step := match goal with - | [ |- appcontext[match ?e with TT => _ | _ => _ end] ] + | [ |- context[match ?e with TT => _ | _ => _ end] ] => invert_one_expr e - | [ |- appcontext[match ?e with Abs _ _ _ => _ end] ] + | [ |- context[match ?e with Abs _ _ _ => _ end] ] => invert_one_expr e - | [ H : appcontext[match ?e with TT => _ | _ => _ end] |- _ ] + | [ H : context[match ?e with TT => _ | _ => _ end] |- _ ] => invert_one_expr e - | [ H : appcontext[match ?e with Abs _ _ _ => _ end] |- _ ] + | [ H : context[match ?e with Abs _ _ _ => _ end] |- _ ] => invert_one_expr e end. diff --git a/src/Compilers/Reify.v b/src/Compilers/Reify.v index 9d3d8544b..810db4d9b 100644 --- a/src/Compilers/Reify.v +++ b/src/Compilers/Reify.v @@ -424,7 +424,7 @@ Ltac Reify_rhs_gen Reify prove_interp_compile_correct interp_op try_tac := clear; abstract ( lazymatch goal with - | [ |- appcontext[@InputSyntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t ?e] ] + | [ |- context[@InputSyntax.Interp ?base_type_code ?interp_base_type ?op ?interp_op ?t ?e] ] => let interp_base_type' := (eval hnf in interp_base_type) in let interp_op' := (eval hnf in interp_op) in change interp_base_type with interp_base_type'; diff --git a/src/Compilers/Z/OpInversion.v b/src/Compilers/Z/OpInversion.v index 58b00c538..e6fc3055b 100644 --- a/src/Compilers/Z/OpInversion.v +++ b/src/Compilers/Z/OpInversion.v @@ -19,9 +19,9 @@ Ltac invert_op := repeat invert_op_step. Ltac invert_match_op_step := match goal with - | [ |- appcontext[match ?e with OpConst _ _ => _ | _ => _ end] ] + | [ |- context[match ?e with OpConst _ _ => _ | _ => _ end] ] => invert_one_op e - | [ H : appcontext[match ?e with OpConst _ _ => _ | _ => _ end] |- _ ] + | [ H : context[match ?e with OpConst _ _ => _ | _ => _ end] |- _ ] => invert_one_op e end. diff --git a/src/LegacyArithmetic/Pow2BaseProofs.v b/src/LegacyArithmetic/Pow2BaseProofs.v index 8a38275dd..681f0b0a9 100644 --- a/src/LegacyArithmetic/Pow2BaseProofs.v +++ b/src/LegacyArithmetic/Pow2BaseProofs.v @@ -280,8 +280,8 @@ Section Pow2BaseProofs. | |- _ => rewrite nth_default_base | |- _ => rewrite IHi | |- _ => rewrite <-Z.lor_shiftl by (rewrite ?Z.pow2_mod_spec; try apply Z.mod_pos_bound; zero_bounds) - | |- appcontext[min ?x ?y] => (rewrite Nat.min_l by omega || rewrite Nat.min_r by omega) - | |- appcontext[2 ^ ?a * _] => rewrite (Z.mul_comm (2 ^ a)); rewrite <-Z.shiftl_mul_pow2 + | |- context[min ?x ?y] => (rewrite Nat.min_l by omega || rewrite Nat.min_r by omega) + | |- context[2 ^ ?a * _] => rewrite (Z.mul_comm (2 ^ a)); rewrite <-Z.shiftl_mul_pow2 | |- _ => solve [auto] | |- _ => lia end. @@ -291,7 +291,7 @@ Section Pow2BaseProofs. | |- _ => progress autorewrite with Ztestbit | |- _ => rewrite Z.testbit_pow2_mod by (omega || trivial) | |- _ => break_if; try omega - | H : ?a < ?b |- appcontext[Z.testbit _ (?a - ?b)] => + | H : ?a < ?b |- context[Z.testbit _ (?a - ?b)] => rewrite (Z.testbit_neg_r _ (a-b)) by omega | |- _ => reflexivity | |- _ => solve [f_equal; ring] diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v index a9987ffde..b49367600 100644 --- a/src/Util/ListUtil.v +++ b/src/Util/ListUtil.v @@ -252,7 +252,7 @@ Ltac boring := simpl; intuition auto with zarith datatypes; repeat match goal with | [ H : _ |- _ ] => rewrite H; clear H - | [ |- appcontext[match ?pf with end] ] => solve [ case pf ] + | [ |- context[match ?pf with end] ] => solve [ case pf ] | _ => progress autounfold in * | _ => progress autorewrite with core | _ => progress simpl in * @@ -633,7 +633,7 @@ Qed. (* grumble, grumble, [rewrite] is bad at inferring the identity function, and constant functions *) Ltac rewrite_rev_combine_update_nth := let lem := match goal with - | [ |- appcontext[update_nth ?n (fun xy => (@?f xy, @?g xy)) (combine ?xs ?ys)] ] + | [ |- context[update_nth ?n (fun xy => (@?f xy, @?g xy)) (combine ?xs ?ys)] ] => let f := match (eval cbv [fst] in (fun y x => f (x, y))) with | fun _ => ?f => f end in @@ -1564,10 +1564,10 @@ Qed. Local Hint Resolve map2_nil_r map2_nil_l. Ltac simpl_list_lengths := repeat match goal with - | H : appcontext[length (@nil ?A)] |- _ => rewrite (@nil_length0 A) in H - | H : appcontext[length (_ :: _)] |- _ => rewrite length_cons in H - | |- appcontext[length (@nil ?A)] => rewrite (@nil_length0 A) - | |- appcontext[length (_ :: _)] => rewrite length_cons + | H : context[length (@nil ?A)] |- _ => rewrite (@nil_length0 A) in H + | H : context[length (_ :: _)] |- _ => rewrite length_cons in H + | |- context[length (@nil ?A)] => rewrite (@nil_length0 A) + | |- context[length (_ :: _)] => rewrite length_cons end. Section OpaqueMap2. diff --git a/src/Util/Tactics/BreakMatch.v b/src/Util/Tactics/BreakMatch.v index f03823a92..95a060750 100644 --- a/src/Util/Tactics/BreakMatch.v +++ b/src/Util/Tactics/BreakMatch.v @@ -70,31 +70,31 @@ Ltac destruct_rewrite_sumbool e := end. Ltac break_match_step only_when := match goal with - | [ |- appcontext[match ?e with _ => _ end] ] + | [ |- context[match ?e with _ => _ end] ] => only_when e; is_var e; destruct e - | [ |- appcontext[match ?e with _ => _ end] ] + | [ |- context[match ?e with _ => _ end] ] => only_when e; match type of e with | sumbool _ _ => destruct_rewrite_sumbool e end - | [ |- appcontext[if ?e then _ else _] ] + | [ |- context[if ?e then _ else _] ] => only_when e; destruct e eqn:? - | [ |- appcontext[match ?e with _ => _ end] ] + | [ |- context[match ?e with _ => _ end] ] => only_when e; destruct e eqn:? | _ => let v := fresh in set_match_refl v only_when; destruct_by_existing_equation v end. Ltac break_match_hyps_step only_when := match goal with - | [ H : appcontext[match ?e with _ => _ end] |- _ ] + | [ H : context[match ?e with _ => _ end] |- _ ] => only_when e; is_var e; destruct e - | [ H : appcontext[match ?e with _ => _ end] |- _ ] + | [ H : context[match ?e with _ => _ end] |- _ ] => only_when e; match type of e with | sumbool _ _ => destruct_rewrite_sumbool e end - | [ H : appcontext[if ?e then _ else _] |- _ ] + | [ H : context[if ?e then _ else _] |- _ ] => only_when e; destruct e eqn:? - | [ H : appcontext[match ?e with _ => _ end] |- _ ] + | [ H : context[match ?e with _ => _ end] |- _ ] => only_when e; destruct e eqn:? | _ => let v := fresh in set_match_refl_hyp v only_when; destruct_by_existing_equation v end. @@ -114,12 +114,12 @@ Ltac break_match_when_head T := repeat break_match_when_head_step T. Ltac break_match_hyps_when_head T := repeat break_match_hyps_when_head_step T. Ltac break_innermost_match_step := break_match_step ltac:(fun v => lazymatch v with - | appcontext[match _ with _ => _ end] => fail + | context[match _ with _ => _ end] => fail | _ => idtac end). Ltac break_innermost_match_hyps_step := break_match_hyps_step ltac:(fun v => lazymatch v with - | appcontext[match _ with _ => _ end] => fail + | context[match _ with _ => _ end] => fail | _ => idtac end). Ltac break_innermost_match := repeat break_innermost_match_step. diff --git a/src/Util/Tactics/Contains.v b/src/Util/Tactics/Contains.v index aa4fddac2..0ee6116e3 100644 --- a/src/Util/Tactics/Contains.v +++ b/src/Util/Tactics/Contains.v @@ -2,12 +2,12 @@ Ltac contains search_for in_term := idtac; lazymatch in_term with - | appcontext[search_for] => idtac + | context[search_for] => idtac end. Ltac free_in x y := idtac; match y with - | appcontext[x] => fail 1 x "appears in" y + | context[x] => fail 1 x "appears in" y | _ => idtac end. diff --git a/src/Util/Tactics/Revert.v b/src/Util/Tactics/Revert.v index 5f549025d..78c94f956 100644 --- a/src/Util/Tactics/Revert.v +++ b/src/Util/Tactics/Revert.v @@ -3,8 +3,8 @@ Ltac revert_last_nondep := match goal with | [ H : _ |- _ ] => lazymatch goal with - | [ H' : appcontext[H] |- _ ] => fail - | [ |- appcontext[H] ] => fail + | [ H' : context[H] |- _ ] => fail + | [ |- context[H] ] => fail | _ => idtac end; revert H diff --git a/src/Util/Tactics/SetEvars.v b/src/Util/Tactics/SetEvars.v index 471d61f60..b55f0edb1 100644 --- a/src/Util/Tactics/SetEvars.v +++ b/src/Util/Tactics/SetEvars.v @@ -1,4 +1,4 @@ Ltac set_evars := repeat match goal with - | [ |- appcontext[?E] ] => is_evar E; let e := fresh "e" in set (e := E) + | [ |- context[?E] ] => is_evar E; let e := fresh "e" in set (e := E) end. diff --git a/src/Util/Tactics/SimplifyProjections.v b/src/Util/Tactics/SimplifyProjections.v index f9b319057..bf9f2d347 100644 --- a/src/Util/Tactics/SimplifyProjections.v +++ b/src/Util/Tactics/SimplifyProjections.v @@ -8,7 +8,7 @@ Ltac pre_simplify_projection proj proj' uproj' := Ltac do_simplify_projection_2Targ_4carg_step proj proj' uproj' construct := change proj' with uproj' at 1; lazymatch goal with - | [ |- appcontext[uproj' _ _ (construct _ _ _ _)] ] + | [ |- context[uproj' _ _ (construct _ _ _ _)] ] => cbv beta iota delta [uproj'] | _ => change uproj' with proj end. diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v index 839defb03..4b19d5f8b 100644 --- a/src/Util/WordUtil.v +++ b/src/Util/WordUtil.v @@ -953,7 +953,7 @@ Lemma wordToNat_wfirstn : forall a b w H, wordToNat (@wfirstn a b w H) = (wordTo Proof. unfold wfirstn. intros; rewrite wordToNat_split1. - match goal with |- appcontext[match ?x with _ => _ end] => generalize x end. + match goal with |- context[match ?x with _ => _ end] => generalize x end. intro H'; destruct H'. reflexivity. Qed. diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index ed09bf828..07466154c 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -251,10 +251,10 @@ Ltac comes_before ls x y := end. Ltac canonicalize_comm_step mul ls comm comm3 := match goal with - | [ |- appcontext[mul ?x ?y] ] + | [ |- context[mul ?x ?y] ] => comes_before ls y x; rewrite (comm x y) - | [ |- appcontext[mul ?x (mul ?y ?z)] ] + | [ |- context[mul ?x (mul ?y ?z)] ] => comes_before ls y x; rewrite (comm3 x y z) end. @@ -437,7 +437,7 @@ Module Z. intros; cbv [Z.pow2_mod]. apply Z.bits_inj'; intros. repeat progress (try break_match; autorewrite with Ztestbit zsimplify; try reflexivity). - try match goal with H : ?a < ?b |- appcontext[Z.testbit _ (?a - ?b)] => + try match goal with H : ?a < ?b |- context[Z.testbit _ (?a - ?b)] => rewrite !Z.testbit_neg_r with (n := a - b) by omega end. autorewrite with Ztestbit; reflexivity. Qed. @@ -2235,7 +2235,7 @@ Module Z. | |- _ => progress intros | |- _ => progress rewrite ?Z.eqb_eq, ?Z.eqb_neq in * | |- _ => progress autorewrite with Ztestbit - | |- appcontext[Z.eqb ?a ?b] => case_eq (Z.eqb a b) + | |- context[Z.eqb ?a ?b] => case_eq (Z.eqb a b) | |- _ => reflexivity || omega end. Qed. -- cgit v1.2.3