diff options
author | Jason Gross <jgross@mit.edu> | 2016-10-09 17:37:55 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-10-10 13:10:32 -0400 |
commit | 9f7ff19fe178823bf94ec532fbdf4e9fa2bfcfa6 (patch) | |
tree | 5b83ba392e5a457d9c781ca477fa082025463ce9 | |
parent | 405f5840e5d9097b034a05d5eeab5ae6ba5757a3 (diff) |
Fix compatibility with sigT notation
-rw-r--r-- | src/ModularArithmetic/ModularBaseSystemOpt.v | 2 | ||||
-rw-r--r-- | src/Util/Notations.v | 2 | ||||
-rw-r--r-- | src/Util/ZUtil.v | 6 |
3 files changed, 5 insertions, 5 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v index 3eef0901e..d1bd49a55 100644 --- a/src/ModularArithmetic/ModularBaseSystemOpt.v +++ b/src/ModularArithmetic/ModularBaseSystemOpt.v @@ -264,7 +264,7 @@ Section Carries. eexists. intros H. rewrite <-carry_gen_opt_correct by assumption. cbv beta iota delta [carry_gen_opt]. - match goal with |- appcontext[?a & Z_ones_opt _] => + match goal with |- appcontext[?a &' Z_ones_opt _] => let LHS := match goal with |- ?LHS = ?RHS => LHS end in let RHS := match goal with |- ?LHS = ?RHS => RHS end in let RHSf := match (eval pattern (a) in RHS) with ?RHSf _ => RHSf end in diff --git a/src/Util/Notations.v b/src/Util/Notations.v index a557c4251..b6aa94971 100644 --- a/src/Util/Notations.v +++ b/src/Util/Notations.v @@ -22,7 +22,7 @@ Reserved Notation "'canonical' 'encoding' 'of' T 'as' B" (at level 50). Reserved Notation "@ 'is_eq_dec' T R" (at level 10, T at level 8, R at level 8). Reserved Infix "<<" (at level 30, no associativity). Reserved Infix ">>" (at level 30, no associativity). -Reserved Infix "&" (at level 50). (* N.B. This conflicts with [{ a : T & P}] for [sigT] *) +Reserved Infix "&'" (at level 50). (* N.B. If we used '&', it would conflict with [{ a : T & P}] for [sigT] *) Reserved Infix "∣" (at level 50). Reserved Infix "~=" (at level 70). Reserved Infix "==" (at level 70, no associativity). diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index c9270e9dd..d82896641 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -13,7 +13,7 @@ Local Open Scope Z. Infix ">>" := Z.shiftr : Z_scope. Infix "<<" := Z.shiftl : Z_scope. -Infix "&" := Z.land : Z_scope. +Infix "&'" := Z.land : Z_scope. Hint Extern 1 => lia : lia. Hint Extern 1 => lra : lra. @@ -230,7 +230,7 @@ Ltac canonicalize_comm_step mul ls comm comm3 := Ltac canonicalize_comm mul ls comm comm3 := repeat canonicalize_comm_step mul ls comm comm3. Module Z. - Definition pow2_mod n i := (n & (Z.ones i)). + Definition pow2_mod n i := (n &' (Z.ones i)). Lemma pow2_mod_spec : forall a b, (0 <= b) -> Z.pow2_mod a b = a mod (2 ^ b). Proof. @@ -337,7 +337,7 @@ Module Z. Qed. Hint Resolve pow2_mod_pos_bound : zarith. - Lemma land_same_r : forall a b, (a & b) & b = a & b. + Lemma land_same_r : forall a b, (a &' b) &' b = a &' b. Proof. intros; apply Z.bits_inj'; intros. rewrite !Z.land_spec. |