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/Specific | |
| 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/Specific')
| -rw-r--r-- | src/Specific/GF25519.v | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v index 471c1d548..6d7e2c38c 100644 --- a/src/Specific/GF25519.v +++ b/src/Specific/GF25519.v @@ -9,6 +9,7 @@ Require Import Crypto.Tactics.VerdiTactics. Require Import Crypto.BaseSystem. Import ListNotations. Require Import Coq.ZArith.ZArith Coq.ZArith.Zpower Coq.ZArith.ZArith Coq.ZArith.Znumtheory. +Require Import Crypto.Util.Notations. Local Open Scope Z. (* BEGIN PseudoMersenneBaseParams instance construction. *) @@ -60,8 +61,8 @@ Proof. (* Uncomment this to see a pretty-printed mulmod Local Transparent Let_In. -Infix "<<" := Z.shiftr (at level 50). -Infix "&" := Z.land (at level 50). +Infix "<<" := Z.shiftr. +Infix "&" := Z.land. Eval cbv beta iota delta [proj1_sig GF25519Base25Point5_mul_reduce_formula Let_In] in fun f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 g0 g1 g2 g3 g4 g5 g6 g7 g8 g9 => proj1_sig ( @@ -122,9 +123,9 @@ Defined. (* Set Printing Depth 1000. Local Transparent Let_In. -Infix "<<" := Z.shiftr (at level 50). -Infix "&" := Z.land (at level 50). +Infix "<<" := Z.shiftr. +Infix "&" := Z.land. Eval cbv beta iota delta [proj1_sig GF25519Base25Point5_freeze_formula Let_In] in fun f0 f1 f2 f3 f4 f5 f6 f7 f8 f9 => proj1_sig ( GF25519Base25Point5_freeze_formula f0 f1 f2 f3 f4 f5 f6 f7 f8 f9). -*)
\ No newline at end of file +*) |