From 18b79f83ce6c947eaa49baf586cc475d50e3d9ca Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 22 Jun 2016 13:34:00 -0700 Subject: Aggregate all level specifications not in Spec/* This prevents notation conflicts (see comment in Notations.v for more explanation). --- src/Specific/GF25519.v | 11 ++++++----- 1 file changed, 6 insertions(+), 5 deletions(-) (limited to 'src/Specific') 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 +*) -- cgit v1.2.3