diff options
| author |  Jason Gross <jagro@google.com> | 2016-06-22 13:34:00 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-06-22 13:34:00 -0700 |
| commit | 18b79f83ce6c947eaa49baf586cc475d50e3d9ca (patch) | |
| tree | dc20511c7507aec0dc8656d30f9388d906ab664b /src/ModularArithmetic/ModularBaseSystemProofs.v | |
| parent | acd8d172e3112372be930544af57c36bf085e6c2 (diff) | |
Aggregate all level specifications not in Spec/*
This prevents notation conflicts (see comment in Notations.v for more
explanation).
Diffstat (limited to 'src/ModularArithmetic/ModularBaseSystemProofs.v')
| -rw-r--r-- | src/ModularArithmetic/ModularBaseSystemProofs.v | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v index 0462b0f37..6f82a8950 100644 --- a/src/ModularArithmetic/ModularBaseSystemProofs.v +++ b/src/ModularArithmetic/ModularBaseSystemProofs.v @@ -6,15 +6,16 @@ Require Import VerdiTactics. Require Crypto.BaseSystem. Require Import Crypto.ModularArithmetic.ModularBaseSystem Crypto.ModularArithmetic.PrimeFieldTheorems. Require Import Crypto.BaseSystemProofs Crypto.ModularArithmetic.PseudoMersenneBaseParams Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs Crypto.ModularArithmetic.ExtendedBaseVector. +Require Import Crypto.Util.Notations. Local Open Scope Z_scope. Section PseudoMersenneProofs. Context `{prm :PseudoMersenneBaseParams}. Local Hint Unfold decode. - Local Notation "u '~=' x" := (rep u x) (at level 70). - Local Notation "u '.+' x" := (add u x) (at level 70). - Local Notation "u '.*' x" := (ModularBaseSystem.mul u x) (at level 70). + Local Notation "u ~= x" := (rep u x). + Local Notation "u .+ x" := (add u x). + Local Notation "u .* x" := (ModularBaseSystem.mul u x). Local Hint Unfold rep. Lemma rep_decode : forall us x, us ~= x -> decode us = x. @@ -256,7 +257,7 @@ End PseudoMersenneProofs. Section CarryProofs. Context `{prm : PseudoMersenneBaseParams}. - Local Notation "u '~=' x" := (rep u x) (at level 70). + Local Notation "u ~= x" := (rep u x). Hint Unfold log_cap. Lemma base_length_lt_pred : (pred (length base) < length base)%nat. @@ -2086,4 +2087,4 @@ Section CanonicalizationProofs. eapply minimal_rep_unique; eauto; rewrite freeze_length; assumption. Qed. -End CanonicalizationProofs.
\ No newline at end of file +End CanonicalizationProofs. |