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. --- src/Util/ZUtil.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'src/Util/ZUtil.v') 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