Aggregate all level specifications not in Spec/*

This prevents notation conflicts (see comment in Notations.v for more
explanation).

10 files changed, 46 insertions, 17 deletions

diff --git a/_CoqProject b/_CoqProject
index 3b2350b77..85aa5a0df 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -40,6 +40,7 @@ src/Util/Decidable.v
 src/Util/IterAssocOp.v
 src/Util/ListUtil.v
 src/Util/NatUtil.v
+src/Util/Notations.v
 src/Util/NumTheoryUtil.v
 src/Util/Tactics.v
 src/Util/Tuple.v
diff --git a/src/BaseSystem.v b/src/BaseSystem.v
index c07aad759..1985520f0 100644
--- a/src/BaseSystem.v
+++ b/src/BaseSystem.v
@@ -2,6 +2,7 @@ Require Import Coq.Lists.List.
 Require Import Coq.ZArith.ZArith Coq.ZArith.Zdiv.
 Require Import Coq.omega.Omega Coq.Numbers.Natural.Peano.NPeano Coq.Arith.Arith.
 Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil.
+Require Import Crypto.Util.Notations.
 Import Nat.
 
 Local Open Scope Z.
@@ -47,7 +48,7 @@ Section BaseSystem.
       | _, nil => us
       | _, _ => vs
     end.
-  Infix ".+" := add (at level 50).
+  Infix ".+" := add.
 
   Hint Extern 1 (@eq Z _ _) => ring.
 
diff --git a/src/BaseSystemProofs.v b/src/BaseSystemProofs.v
index 4414877b4..85835aabe 100644
--- a/src/BaseSystemProofs.v
+++ b/src/BaseSystemProofs.v
@@ -3,9 +3,10 @@ Require Import Util.ListUtil Util.CaseUtil Util.ZUtil.
 Require Import ZArith.ZArith ZArith.Zdiv.
 Require Import Omega NPeano Arith.
 Require Import Crypto.BaseSystem.
+Require Import Crypto.Util.Notations.
 Local Open Scope Z.
 
-Local Infix ".+" := add (at level 50).
+Local Infix ".+" := add.
 
 Local Hint Extern 1 (@eq Z _ _) => ring.
 
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index 683addd5d..c217303aa 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -7,6 +7,7 @@ Require Import Crypto.Tactics.VerdiTactics.
 Require Import Coq.Classes.Morphisms.
 Require Import Relation_Definitions.
 Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Notations.
 
 Module E.
   Import Group Ring Field CompleteEdwardsCurve.E.
@@ -18,7 +19,7 @@ Module E.
     Local Notation "0" := Fzero.  Local Notation "1" := Fone.
     Local Infix "+" := Fadd. Local Infix "*" := Fmul.
     Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
-    Local Notation "x ^2" := (x*x) (at level 30).
+    Local Notation "x ^2" := (x*x).
     Local Notation point := (@point F Feq Fone Fadd Fmul a d).
     Local Notation onCurve := (@onCurve F Feq Fone Fadd Fmul a d).
 
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
index 25af83a0a..e2ffa0313 100644
--- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
@@ -7,6 +7,7 @@ Require Import Crypto.Tactics.VerdiTactics.
 Require Import Coq.Classes.Morphisms.
 Require Import Relation_Definitions.
 Require Import Crypto.Util.Tuple.
+Require Import Crypto.Util.Notations.
 
 Module Extended.
   Section ExtendedCoordinates.
@@ -18,7 +19,7 @@ Module Extended.
     Local Notation "0" := Fzero.  Local Notation "1" := Fone.
     Local Infix "+" := Fadd. Local Infix "*" := Fmul.
     Local Infix "-" := Fsub. Local Infix "/" := Fdiv.
-    Local Notation "x ^2" := (x*x) (at level 30).
+    Local Notation "x ^2" := (x*x).
     Local Notation Epoint := (@E.point F Feq Fone Fadd Fmul a d).
     Local Notation onCurve := (@Pre.onCurve F Feq Fone Fadd Fmul a d).
 
diff --git a/src/CompleteEdwardsCurve/Pre.v b/src/CompleteEdwardsCurve/Pre.v
index 5314ee37c..7e9f14321 100644
--- a/src/CompleteEdwardsCurve/Pre.v
+++ b/src/CompleteEdwardsCurve/Pre.v
@@ -1,5 +1,6 @@
 Require Import Coq.Classes.Morphisms. Require Coq.Setoids.Setoid.
 Require Import Crypto.Algebra Crypto.Tactics.Nsatz.
+Require Import Crypto.Util.Notations.
 
 Generalizable All Variables.
 Section Pre.
@@ -9,7 +10,7 @@ Section Pre.
   Local Notation "0" := zero.  Local Notation "1" := one.
   Local Infix "+" := add. Local Infix "*" := mul.
   Local Infix "-" := sub. Local Infix "/" := div.
-  Local Notation "x '^' 2" := (x*x) (at level 30).
+  Local Notation "x ^2" := (x*x).
 
   Add Field EdwardsCurveField : (Field.field_theory_for_stdlib_tactic (T:=F)).
 
@@ -97,4 +98,4 @@ Section RespectsFieldHomomorphism.
       apply conj;
       (rewrite_strat topdown hints field_homomorphism); reflexivity.
   Qed.
-End RespectsFieldHomomorphism.
\ No newline at end of file
+End RespectsFieldHomomorphism.
diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v
index ca8c19d18..08545bdb4 100644
--- a/src/ModularArithmetic/ModularBaseSystem.v
+++ b/src/ModularArithmetic/ModularBaseSystem.v
@@ -7,6 +7,7 @@ Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
 Require Import Crypto.ModularArithmetic.ExtendedBaseVector.
 Require Import Crypto.Tactics.VerdiTactics.
+Require Import Crypto.Util.Notations.
 Local Open Scope Z_scope.
 
 Section PseudoMersenneBase.
@@ -15,7 +16,7 @@ Section PseudoMersenneBase.
   Definition decode (us : digits) : F modulus := ZToField (BaseSystem.decode base us).
 
   Definition rep (us : digits) (x : F modulus) := (length us = length base)%nat /\ decode us = x.
-  Local Notation "u '~=' x" := (rep u x) (at level 70).
+  Local Notation "u ~= x" := (rep u x).
   Local Hint Unfold rep.
 
   Definition encode (x : F modulus) := encode x ++ BaseSystem.zeros (length base - 1)%nat.
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.
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
+*)
diff --git a/src/Util/Notations.v b/src/Util/Notations.v
new file mode 100644
index 000000000..6cc80944b
--- /dev/null
+++ b/src/Util/Notations.v
@@ -0,0 +1,20 @@
+(** * Reserved Notations *)
+
+(** Putting them all together in one file prevents conflicts.  Coq's
+    parser (camlpX) is really bad at conflicting notation levels and
+    is sometimes really bad at backtracking, too.  Not having level
+    declarations in other files makes it harder for us to confuse
+    Coq's parser. *)
+
+Reserved Infix "=?" (at level 70, no associativity).
+Reserved Infix "?=" (at level 70, no associativity).
+Reserved Infix "?<" (at level 70, no associativity).
+Reserved Infix ".+" (at level 50).
+Reserved Notation "x ^2" (at level 30, format "x ^2").
+Reserved Infix "mod" (at level 40, no associativity).
+Reserved Notation "'canonical' 'encoding' 'of' T 'as' B" (at level 50).
+Reserved Infix "<<" (at level 50).
+Reserved Infix "&" (at level 50).
+Reserved Infix "<<" (at level 50).
+Reserved Infix "&" (at level 50).
+Reserved Infix "~=" (at level 70).