Move most notation level declarations into Util

This reveals and prevents notation clashes.

Notable breakage:
- `x {{ y }}` breaks `Context {forall x, {P x} + {~P x}}.`
  (@jadephilipoom)
- `x [[ y ]]` breaks `destruct x as [[a]|[b]].` (@jadephilipoom)
- `O :( A , B ): :?: L ::: R` breaks `((1):nat)` and `constr:(nat)`
  (@varomodt)

After    | File Name                                         | Before   || Change
------------------------------------------------------------------------------------
3m16.07s | Total                                             | 3m23.63s || -0m07.55s
------------------------------------------------------------------------------------
0m16.90s | ModularArithmetic/ModularBaseSystemProofs         | 0m19.02s || -0m02.12s
0m03.29s | ModularArithmetic/ModularBaseSystemOpt            | 0m05.30s || -0m02.00s
0m12.04s | Experiments/SpecEd25519                           | 0m13.89s || -0m01.85s
0m36.02s | CompleteEdwardsCurve/ExtendedCoordinates          | 0m36.12s || -0m00.09s
0m34.48s | Specific/GF25519                                  | 0m34.27s || +0m00.20s
0m15.62s | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems | 0m15.76s || -0m00.14s
0m07.36s | Specific/GF1305                                   | 0m07.34s || +0m00.02s
0m06.64s | Algebra                                           | 0m06.14s || +0m00.50s
0m05.12s | WeierstrassCurve/Pre                              | 0m05.09s || +0m00.03s
0m04.58s | ModularArithmetic/Tutorial                        | 0m03.83s || +0m00.75s
0m04.46s | BaseSystemProofs                                  | 0m04.33s || +0m00.12s
0m04.26s | ModularArithmetic/Pow2BaseProofs                  | 0m05.16s || -0m00.90s
0m03.91s | CompleteEdwardsCurve/Pre                          | 0m04.62s || -0m00.71s
0m02.75s | Assembly/State                                    | 0m03.12s || -0m00.37s
0m02.55s | Experiments/EdDSARefinement                       | 0m01.85s || +0m00.69s
0m02.46s | Util/ZUtil                                        | 0m02.45s || +0m00.00s
0m01.86s | Assembly/Wordize                                  | 0m02.02s || -0m00.15s
0m01.68s | ModularArithmetic/ModularArithmeticTheorems       | 0m01.68s || +0m00.00s
0m01.67s | ModularArithmetic/PrimeFieldTheorems              | 0m01.96s || -0m00.29s
0m01.50s | Encoding/PointEncodingPre                         | 0m02.20s || -0m00.70s
0m01.46s | ModularArithmetic/BarrettReduction/Z              | 0m01.02s || +0m00.43s
0m01.26s | BaseSystem                                        | 0m01.21s || +0m00.05s
0m01.24s | Assembly/Pseudize                                 | 0m01.22s || +0m00.02s
0m01.20s | ModularArithmetic/ExtendedBaseVector              | 0m01.86s || -0m00.66s
0m01.04s | Util/IterAssocOp                                  | 0m00.74s || +0m00.30s
0m00.96s | ModularArithmetic/ExtPow2BaseMulProofs            | 0m00.67s || +0m00.28s
0m00.96s | Assembly/Pipeline                                 | 0m00.65s || +0m00.30s
0m00.93s | Experiments/DerivationsOptionRectLetInEncoding    | 0m00.98s || -0m00.04s
0m00.93s | ModularArithmetic/ModularBaseSystemField          | 0m00.95s || -0m00.01s
0m00.92s | Util/NumTheoryUtil                                | 0m01.19s || -0m00.26s
0m00.90s | ModularArithmetic/ModularBaseSystemListProofs     | 0m00.89s || +0m00.01s
0m00.82s | ModularArithmetic/PseudoMersenneBaseParamProofs   | 0m00.95s || -0m00.13s
0m00.81s | Assembly/QhasmEvalCommon                          | 0m00.86s || -0m00.04s
0m00.80s | Assembly/StringConversion                         | 0m00.60s || +0m00.20s
0m00.79s | Assembly/Qhasm                                    | 0m00.54s || +0m00.25s
0m00.73s | Assembly/Pseudo                                   | 0m00.98s || -0m00.25s
0m00.72s | Util/AdditionChainExponentiation                  | 0m00.92s || -0m00.20s
0m00.69s | Experiments/SpecificCurve25519                    | 0m00.72s || -0m00.03s
0m00.65s | Spec/ModularWordEncoding                          | 0m00.85s || -0m00.19s
0m00.65s | ModularArithmetic/ModularBaseSystemList           | 0m00.68s || -0m00.03s
0m00.65s | Assembly/PseudoConversion                         | 0m00.67s || -0m00.02s
0m00.64s | Encoding/ModularWordEncodingPre                   | 0m00.62s || +0m00.02s
0m00.64s | Spec/EdDSA                                        | 0m00.93s || -0m00.29s
0m00.64s | Testbit                                           | 0m00.94s || -0m00.29s
0m00.63s | Encoding/ModularWordEncodingTheorems              | 0m00.66s || -0m00.03s
0m00.62s | Assembly/AlmostQhasm                              | 0m00.49s || +0m00.13s
0m00.59s | ModularArithmetic/ModularBaseSystem               | 0m00.61s || -0m00.02s
0m00.49s | Spec/WeierstrassCurve                             | 0m00.43s || +0m00.06s
0m00.49s | Assembly/QhasmUtil                                | 0m00.51s || -0m00.02s
0m00.49s | ModularArithmetic/Pre                             | 0m00.47s || +0m00.02s
0m00.47s | Assembly/Vectorize                                | 0m00.51s || -0m00.04s
0m00.46s | Assembly/AlmostConversion                         | 0m00.44s || +0m00.02s
0m00.42s | ModularArithmetic/Pow2Base                        | 0m00.42s || +0m00.00s
0m00.41s | ModularArithmetic/PseudoMersenneBaseParams        | 0m00.45s || -0m00.04s
0m00.41s | Spec/ModularArithmetic                            | 0m00.41s || +0m00.00s
0m00.39s | Spec/CompleteEdwardsCurve                         | 0m00.41s || -0m00.01s
0m00.03s | Util/Notations                                    | 0m00.03s || +0m00.00s

14 files changed, 115 insertions, 77 deletions

diff --git a/src/Algebra.v b/src/Algebra.v
index f4afcb935..9bd3cac5e 100644
--- a/src/Algebra.v
+++ b/src/Algebra.v
@@ -9,12 +9,11 @@ Require Export Crypto.Util.FixCoqMistakes.
 
 Module Import ModuloCoq8485.
   Import NPeano Nat.
-  Infix "mod" := modulo (at level 40, no associativity).
+  Infix "mod" := modulo.
 End ModuloCoq8485.
 
 Notation is_eq_dec := (DecidableRel _) (only parsing).
-Notation "@ 'is_eq_dec' T R" := (DecidableRel (R:T->T->Prop))
-                                  (at level 10, T at level 8, R at level 8, only parsing).
+Notation "@ 'is_eq_dec' T R" := (DecidableRel (R:T->T->Prop)) (only parsing).
 Notation eq_dec x y := (@dec (_ x y) _) (only parsing).
 Notation "x =? y" := (eq_dec x y) : type_scope.
 
@@ -305,7 +304,7 @@ Module Group.
     Lemma surjective_homomorphism_from_group
           {G EQ OP ID INV} {groupG:@group G EQ OP ID INV}
           {H eq op id inv}
-          {Equivalence_eq: @Equivalence H eq} {eq_dec: forall x y, {eq x y} + {~ eq x y}}
+          {Equivalence_eq: @Equivalence H eq} {eq_dec: forall x y, {eq x y} + {~ eq x y} }
           {Proper_op:Proper(eq==>eq==>eq)op}
           {Proper_inv:Proper(eq==>eq)inv}
           {phi iph} {Proper_phi:Proper(EQ==>eq)phi} {Proper_iph:Proper(eq==>EQ)iph}
@@ -330,7 +329,7 @@ Module Group.
 
     Lemma isomorphism_to_subgroup_group
           {G EQ OP ID INV}
-          {Equivalence_EQ: @Equivalence G EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y}}
+          {Equivalence_EQ: @Equivalence G EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y} }
           {Proper_OP:Proper(EQ==>EQ==>EQ)OP}
           {Proper_INV:Proper(EQ==>EQ)INV}
           {H eq op id inv} {groupG:@group H eq op id inv}
@@ -534,7 +533,7 @@ Module Ring.
 
   Lemma isomorphism_to_subring_ring
         {T EQ ZERO ONE OPP ADD SUB MUL}
-        {Equivalence_EQ: @Equivalence T EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y}}
+        {Equivalence_EQ: @Equivalence T EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y} }
         {Proper_OPP:Proper(EQ==>EQ)OPP}
         {Proper_ADD:Proper(EQ==>EQ==>EQ)ADD}
         {Proper_SUB:Proper(EQ==>EQ==>EQ)SUB}
@@ -664,7 +663,7 @@ Module Field.
 
   Lemma isomorphism_to_subfield_field
         {T EQ ZERO ONE OPP ADD SUB MUL INV DIV}
-        {Equivalence_EQ: @Equivalence T EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y}}
+        {Equivalence_EQ: @Equivalence T EQ} {eq_dec: forall x y, {EQ x y} + {~ EQ x y} }
         {Proper_OPP:Proper(EQ==>EQ)OPP}
         {Proper_ADD:Proper(EQ==>EQ==>EQ)ADD}
         {Proper_SUB:Proper(EQ==>EQ==>EQ)SUB}
diff --git a/src/Assembly/Pipeline.v b/src/Assembly/Pipeline.v
index 8e58e7345..87102cca8 100644
--- a/src/Assembly/Pipeline.v
+++ b/src/Assembly/Pipeline.v
@@ -1,8 +1,9 @@
 Require Import Bedrock.Word.
-Require Import QhasmCommon QhasmEvalCommon.
-Require Import Pseudo Qhasm AlmostQhasm Conversion Language.
-Require Import PseudoConversion AlmostConversion StringConversion.
-Require Import Wordize Vectorize Pseudize.
+Require Import Crypto.Assembly.QhasmCommon Crypto.Assembly.QhasmEvalCommon.
+Require Import Crypto.Assembly.Pseudo Crypto.Assembly.Qhasm Crypto.Assembly.AlmostQhasm Crypto.Assembly.Conversion Crypto.Assembly.Language.
+Require Import Crypto.Assembly.PseudoConversion Crypto.Assembly.AlmostConversion Crypto.Assembly.StringConversion.
+Require Import Crypto.Assembly.Wordize Crypto.Assembly.Vectorize Crypto.Assembly.Pseudize.
+Require Import Crypto.Util.Notations.
 
 Module Pipeline.
   Export AlmostQhasm Qhasm QhasmString.
@@ -24,8 +25,8 @@ End Pipeline.
 Module PipelineExamples.
   Import Pipeline ListNotations StateCommon EvalUtil ListState.
 
-  Local Notation "v [[ i ]]" := (nth i v (wzero _)) (at level 40).
-  Local Notation "$$ v" := (natToWord _ v) (at level 40).
+  Local Notation "v [[ i ]]" := (nth i v (wzero _)).
+  Local Notation "$$ v" := (natToWord _ v).
 
   (*
   Definition add_example: @pseudeq 32 W32 1 1 (fun v =>
@@ -53,7 +54,7 @@ Module PipelineExamples.
       plet b := v[[0]] in
 
       (* NOTE: we want the lets in this format to unify with
-               pseudo_mult_dual *)  
+               pseudo_mult_dual *)
       plet c := multHigh a b in
       plet d := a ^* b in
 
diff --git a/src/Assembly/Pseudo.v b/src/Assembly/Pseudo.v
index b8aae4521..ca4700a7f 100644
--- a/src/Assembly/Pseudo.v
+++ b/src/Assembly/Pseudo.v
@@ -1,6 +1,7 @@
 Require Import Crypto.Assembly.QhasmCommon Crypto.Assembly.QhasmUtil Crypto.Assembly.State.
 Require Import Crypto.Assembly.Language Crypto.Assembly.QhasmEvalCommon.
 Require Import Coq.Lists.List Coq.Arith.Compare_dec Coq.omega.Omega.
+Require Import Crypto.Util.Notations.
 Require Export Crypto.Util.FixCoqMistakes.
 
 Module Pseudo <: Language.
@@ -31,8 +32,8 @@ Module Pseudo <: Language.
   }.
 
   Definition Params := Params'.
-  Definition State (p: Params): Type := ListState (width p).
-  Definition Program (p: Params): Type :=
+  Definition State (p: Params) : Type := ListState (width p).
+  Definition Program (p: Params) : Type :=
     @Pseudo (width p) (spec p) (inputs p) (outputs p).
 
   Definition Unary32: Params := mkParams 32 W32 1 1.
@@ -40,7 +41,7 @@ Module Pseudo <: Language.
 
   (* Evaluation *)
 
-  Fixpoint pseudoEval {n m w s} (prog: @Pseudo w s n m) (st: ListState w): option (ListState w) :=
+  Fixpoint pseudoEval {n m w s} (prog: @Pseudo w s n m) (st: ListState w) : option (ListState w) :=
     match prog with
     | PVar n _ i => omap (getVar i st) (fun x => Some (setList [x] st))
     | PMem n m v i => omap (getMem v i st) (fun x => Some (setList [x] st))
@@ -114,7 +115,7 @@ Module Pseudo <: Language.
   Delimit Scope pseudo_notations with p.
   Local Open Scope pseudo_notations.
 
-  Definition indexize {n: nat} (x: nat): Index n.
+  Definition indexize {n: nat} (x: nat) : Index n.
     intros; destruct (le_dec n 0).
 
     - exists 0; abstract intuition auto with zarith.
@@ -123,60 +124,65 @@ Module Pseudo <: Language.
   Defined.
 
   Notation "% A" := (PVar _ (Some false) (indexize A))
-    (at level 20, right associativity) : pseudo_notations.
+    : pseudo_notations.
 
   Notation "$ A" := (PVar _ (Some true) (indexize A))
-    (at level 20, right associativity) : pseudo_notations.
+    : pseudo_notations.
 
   Notation "A :[ B ]:" :=  (PMem _ _ (indexize A) (indexize B))
-    (at level 20, right associativity) : pseudo_notations.
+    : pseudo_notations.
 
   Notation "# A" := (PConst _ (natToWord _ A))
-    (at level 20, right associativity) : pseudo_notations.
+    : pseudo_notations.
 
   Notation "A :+: B" := (PBin _ IAdd (PComb _ _ _ A B))
-    (at level 60, right associativity) : pseudo_notations.
+    : pseudo_notations.
 
   Notation "A :+c: B" := (PCarry _ AddWithCarry (PComb _ _ _ A B))
-    (at level 60, right associativity) : pseudo_notations.
+    : pseudo_notations.
 
   Notation "A :-: B" := (PBin _ ISub (PComb _ _ _ A B))
-    (at level 60, right associativity) : pseudo_notations.
+    : pseudo_notations.
 
   Notation "A :&: B" := (PBin _ IAnd (PComb _ _ _ A B))
-    (at level 45, right associativity) : pseudo_notations.
+    : pseudo_notations.
 
   Notation "A :^: B" := (PBin _ IXor (PComb _ _ _ A B))
-    (at level 45, right associativity) : pseudo_notations.
+    : pseudo_notations.
 
   Notation "A :>>: B" := (PShift _ Shr (indexize B) A)
-    (at level 60, right associativity) : pseudo_notations.
+    : pseudo_notations.
 
   Notation "A :<<: B" := (PShift _ Shl (indexize B) A)
-    (at level 60, right associativity) : pseudo_notations.
+    : pseudo_notations.
 
   Notation "A :*: B" := (PDual _ Mult (PComb _ _ _ A B))
-    (at level 55, right associativity) : pseudo_notations.
+    : pseudo_notations.
 
+  (* TODO(rsloan, from jgross): This notation is not okay.  It breaks
+     [constr:(nat)] and [((1):nat)].  Please remove all frowny faces
+     from notations, and then move [Reserved Notation] line to
+     Fiat.Crypto.Util.Notations. *)
+  Reserved Notation "O :( A , B ): :?: L ::: R" (at level 70, right associativity).
   Notation "O :( A , B ): :?: L ::: R" :=
     (PIf _ _ O (indexize A) (indexize B) L R)
-    (at level 70, right associativity) : pseudo_notations.
+    : pseudo_notations.
 
   Notation "F :**: e" :=
     (PFunExp _ F e)
-    (at level 70, right associativity) : pseudo_notations.
+    : pseudo_notations.
 
   Notation "E :->: F" :=
     (PLet _ _ _ E F)
-    (at level 70, right associativity) : pseudo_notations.
+    : pseudo_notations.
 
   Notation "A :|: B" :=
     (PComb _ _ _ A B)
-    (at level 65, left associativity) : pseudo_notations.
+    : pseudo_notations.
 
   Notation "n ::: A :():" :=
     (PCall _ _ n A)
-    (at level 65, left associativity) : pseudo_notations.
+    : pseudo_notations.
 
   Close Scope pseudo_notations.
 End Pseudo.
diff --git a/src/Assembly/QhasmUtil.v b/src/Assembly/QhasmUtil.v
index 1ab894e94..53e9cf573 100644
--- a/src/Assembly/QhasmUtil.v
+++ b/src/Assembly/QhasmUtil.v
@@ -1,40 +1,41 @@
 Require Import Coq.ZArith.ZArith Coq.NArith.NArith Coq.Numbers.Natural.Peano.NPeano.
 Require Import Crypto.Assembly.QhasmCommon.
+Require Import Crypto.Util.Notations.
 Require Export Bedrock.Word.
 Require Export Crypto.Util.FixCoqMistakes.
 
 Delimit Scope nword_scope with w.
 Local Open Scope nword_scope.
 
-Notation "& x" := (wordToN x) (at level 30) : nword_scope.
-Notation "** x" := (NToWord _ x) (at level 30) : nword_scope.
+Notation "& x" := (wordToN x) : nword_scope.
+Notation "** x" := (NToWord _ x) : nword_scope.
 
 Section Util.
-  Definition convS {A B: Set} (x: A) (H: A = B): B :=
+  Definition convS {A B: Set} (x: A) (H: A = B) : B :=
     eq_rect A (fun B0 : Set => B0) x B H.
 
-  Definition high {k n: nat} (p: (k <= n)%nat) (w: word n): word k.
+  Definition high {k n: nat} (p: (k <= n)%nat) (w: word n) : word k.
     refine (split1 k (n - k) (convS w _)).
     abstract (replace n with (k + (n - k)) by omega; intuition auto with arith).
   Defined.
 
-  Definition low {k n: nat} (p: (k <= n)%nat) (w: word n): word k.
+  Definition low {k n: nat} (p: (k <= n)%nat) (w: word n) : word k.
     refine (split2 (n - k) k (convS w _)).
     abstract (replace n with (k + (n - k)) by omega; intuition auto with zarith).
   Defined.
 
-  Definition extend {k n: nat} (p: (k <= n)%nat) (w: word k): word n.
+  Definition extend {k n: nat} (p: (k <= n)%nat) (w: word k) : word n.
     refine (convS (zext w (n - k)) _).
     abstract (replace (k + (n - k)) with n by omega; intuition).
   Defined.
 
-  Definition shiftr {n} (w: word n) (k: nat): word n :=
+  Definition shiftr {n} (w: word n) (k: nat) : word n :=
     match (le_dec k n) with
     | left p => extend p (high p w)
     | right _ => wzero n
     end.
 
-  Definition mask {n} (k: nat) (w: word n): word n :=
+  Definition mask {n} (k: nat) (w: word n) : word n :=
     match (le_dec k n) with
     | left p => extend p (low p w)
     | right _ => w
@@ -58,7 +59,7 @@ Section Util.
         end).
   Defined.
 
-  Definition break {n} (m: nat) (x: word n): word m * word (n - m).
+  Definition break {n} (m: nat) (x: word n) : word m * word (n - m).
     refine match (le_dec m n) with
     | left p => (extend _ (low p x), extend _ (@high (n - m) n _ x))
     | right p => (extend _ x, _)
@@ -67,13 +68,13 @@ Section Util.
     replace (n - m) with O by abstract omega; exact WO.
   Defined.
 
-  Definition addWithCarry {n} (x y: word n) (c: bool): word n :=
+  Definition addWithCarry {n} (x y: word n) (c: bool) : word n :=
     x ^+ y ^+ (natToWord _ (if c then 1 else 0)).
 
   Definition omap {A B} (x: option A) (f: A -> option B) :=
     match x with | Some y => f y | _ => None end.
 
-  Notation "A <- X ; B" := (omap X (fun A => B)) (at level 70, right associativity).
+  Notation "A <- X ; B" := (omap X (fun A => B)).
 End Util.
 
 Close Scope nword_scope.
diff --git a/src/Assembly/Vectorize.v b/src/Assembly/Vectorize.v
index 4eed28aad..08e9ee356 100644
--- a/src/Assembly/Vectorize.v
+++ b/src/Assembly/Vectorize.v
@@ -1,20 +1,21 @@
 Require Export Bedrock.Word Bedrock.Nomega.
 Require Import Coq.Numbers.Natural.Peano.NPeano Coq.NArith.NArith Coq.PArith.PArith Coq.NArith.Ndigits Coq.Arith.Compare_dec Coq.Arith.Arith.
 Require Import Coq.Logic.ProofIrrelevance Coq.setoid_ring.Ring Coq.Lists.List Coq.omega.Omega.
+Require Import Crypto.Util.Notations.
 
 Require Export Crypto.Util.FixCoqMistakes.
 
 Definition Let_In {A P} (x : A) (f : forall a : A, P a) : P x :=
   let y := x in f y.
 
-Notation "'plet' x := y 'in' z" := (Let_In y (fun x => z)) (at level 60).
+Notation "'plet' x := y 'in' z" := (Let_In y (fun x => z)).
 
 Section Vector.
   Import ListNotations.
 
   Definition vec T n := {x: list T | length x = n}.
 
-  Definition vget {n T} (x: vec T n) (i: {v: nat | (v < n)%nat}): T.
+  Definition vget {n T} (x: vec T n) (i: {v: nat | (v < n)%nat}) : T.
     refine (
       match (proj1_sig x) as x' return (proj1_sig x) = x' -> _ with
       | [] => fun _ => _
diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
index dbfdb023e..716d72b3e 100644
--- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
+++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v
@@ -34,7 +34,7 @@ Module E.
                let x := fresh "x" p in
                let y := fresh "y" p in
                let pf := fresh "pf" p in
-               destruct p as [[x y] pf]
+               destruct p as [ [x y] pf]
              end.
 
     Local Obligation Tactic := intros; destruct_points; simpl; super_nsatz.
@@ -155,7 +155,7 @@ Module E.
     Program Definition ref_phi (P:Fpoint) : Kpoint := exist _ (
       let (x, y) := coordinates P in (phi x, phi y)) _.
     Next Obligation.
-      destruct P as [[? ?] ?]; simpl.
+      destruct P as [ [? ?] ?]; simpl.
       rewrite_strat bottomup hints field_homomorphism.
       eauto using is_homomorphism_phi_proper; assumption.
     Qed.
@@ -171,7 +171,7 @@ Module E.
              | |- _ => intro
              | |-  _ /\ _ => split
              | [H: _ /\ _ |- _ ] => destruct H
-             | [p: point |- _ ] => destruct p as [[??]?]
+             | [p: point |- _ ] => destruct p as [ [??]?]
              | |- context[point_phi] => setoid_rewrite point_phi_correct
              | |- _ => progress cbv [fst snd coordinates proj1_sig eq fieldwise fieldwise' add zero opp ref_phi] in *
              | |- Keq ?x ?x => reflexivity
diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
index ac3523889..6b28173e3 100644
--- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v
+++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v
@@ -39,8 +39,8 @@ Module Extended.
              | |- Proper _ _ => intro
              | _ => progress intros
              | [ H: _ /\ _ |- _ ] => destruct H
-             | [ p:E.point |- _ ] => destruct p as [[??]?]
-             | [ p:point |- _ ] => destruct p as [[[[??]?]?]?]
+             | [ p:E.point |- _ ] => destruct p as [ [??] ? ]
+             | [ p:point |- _ ] => destruct p as [ [ [ [??] ? ] ? ] ? ]
              | _ => progress autounfold with bash in *
              | |- _ /\ _ => split
              | _ => solve [neq01]
@@ -98,7 +98,7 @@ Module Extended.
         let (x, y) := E.coordinates (E.add (to_twisted P) (to_twisted Q)) in
         (fieldwise (n:=2) Feq) (x, y) (X/Z, Y/Z).
       Proof.
-        destruct P as [[[[]?]?][HP []]]; destruct Q as [[[[]?]?][HQ []]].
+        destruct P as [ [ [ [ ] ? ] ? ] [ HP [ ] ] ]; destruct Q as [ [ [ [ ] ? ] ? ] [ HQ [ ] ] ].
         pose proof edwardsAddCompletePlus (a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) _ _ _ _ HP HQ.
         pose proof edwardsAddCompleteMinus (a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) _ _ _ _ HP HQ.
         bash.
@@ -110,7 +110,7 @@ Module Extended.
         intros.
         pose proof (add_coordinates_correct P Q) as Hrep.
         pose proof Pre.unifiedAdd'_onCurve(a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) (E.coordinates (to_twisted P)) (E.coordinates (to_twisted Q)) as Hon.
-        destruct P as [[[[]?]?][HP []]]; destruct Q as [[[[]?]?][HQ []]].
+        destruct P as [ [ [ [ ] ? ] ? ] [ HP [ ] ] ]; destruct Q as [ [ [ [ ] ? ] ? ] [ HQ [ ] ] ].
         pose proof edwardsAddCompletePlus (a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) _ _ _ _ HP HQ as Hnz1.
         pose proof edwardsAddCompleteMinus (a_nonzero:=E.nonzero_a)(a_square:=E.square_a)(d_nonsquare:=E.nonsquare_d)(char_gt_2:=E.char_gt_2) _ _ _ _ HP HQ as Hnz2.
         autounfold with bash in *; simpl in *.
@@ -122,7 +122,7 @@ Module Extended.
       Lemma to_twisted_add P Q : E.eq (to_twisted (add P Q)) (E.add (to_twisted P) (to_twisted Q)).
       Proof.
         pose proof (add_coordinates_correct P Q) as Hrep.
-        destruct P as [[[[]?]?][HP []]]; destruct Q as [[[[]?]?][HQ []]].
+        destruct P as [ [ [ [ ] ? ] ? ] [ HP [ ] ] ]; destruct Q as [ [ [ [ ] ? ] ? ] [ HQ [ ] ] ].
         autounfold with bash in *; simpl in *.
         destruct Hrep as [HA HB]. rewrite <-!HA, <-!HB; clear HA HB.
         split; reflexivity.
@@ -230,7 +230,7 @@ Module Extended.
     Program Definition ref_phi (P:Fpoint) : Kpoint := exist _ (
       let '(X, Y, Z, T) := coordinates P in (phi X, phi Y, phi Z, phi T)) _.
     Next Obligation.
-      destruct P as [[[[] ?] ?] [? [? ?]]]; unfold onCurve in *; simpl.
+      destruct P as [ [ [ [ ] ? ] ? ] [ ? [ ? ? ] ] ]; unfold onCurve in *; simpl.
       (rewrite_strat bottomup hints field_homomorphism); try assumption.
       eauto 10 using is_homomorphism_phi_proper, phi_nonzero.
     Qed.
@@ -246,7 +246,7 @@ Module Extended.
              | |- _ => intro
              | |-  _ /\ _ => split
              | [H: _ /\ _ |- _ ] => destruct H
-             | [p: point |- _ ] => destruct p as [[[[] ?] ?] [? [? ?]]]
+             | [p: point |- _ ] => destruct p as [ [ [ [ ] ? ] ? ] [ ? [ ? ? ] ] ]
              | |- context[point_phi] => setoid_rewrite point_phi_correct
              | |- _ => progress cbv [fst snd coordinates proj1_sig eq to_twisted E.eq E.coordinates fieldwise fieldwise' add add_coordinates ref_phi] in *
              | |- Keq ?x ?x => reflexivity
diff --git a/src/Encoding/PointEncodingPre.v b/src/Encoding/PointEncodingPre.v
index e6305f798..f9eb96072 100644
--- a/src/Encoding/PointEncodingPre.v
+++ b/src/Encoding/PointEncodingPre.v
@@ -11,21 +11,22 @@ Require Import Crypto.Algebra.
 
 Require Import Crypto.Spec.Encoding Crypto.Spec.ModularWordEncoding Crypto.Spec.ModularArithmetic.
 
+Require Import Crypto.Util.Notations.
 Require Export Crypto.Util.FixCoqMistakes.
 
 Generalizable All Variables.
 Section PointEncodingPre.
   Context {F eq zero one opp add sub mul inv div} `{field F eq zero one opp add sub mul inv div}.
-  Local Infix "==" := eq (at level 30) : type_scope.
-  Local Notation "a !== b" := (not (a == b)) (at level 30): type_scope.
+  Local Infix "==" := eq : type_scope.
+  Local Notation "a !== b" := (not (a == b)): type_scope.
   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)).
 
-  Context {eq_dec:forall x y : F, {x==y}+{x==y->False}}.
+  Context {eq_dec:forall x y : F, {x==y}+{x==y->False} }.
   Definition F_eqb x y := if eq_dec x y then true else false.
   Lemma F_eqb_iff : forall x y, F_eqb x y = true <-> x == y.
   Proof.
@@ -368,7 +369,7 @@ Proof.
   break_match.
   + f_equal.
     apply option_point_eq_iff.
-    destruct p as [[? ?] ?]; simpl in *.
+    destruct p as [ [ ? ? ] ? ]; simpl in *.
     assumption.
   + exfalso; apply  n.
     eapply option_coordinates_eq_trans; [ | eauto using option_coordinates_eq_sym ].
diff --git a/src/Experiments/EdDSARefinement.v b/src/Experiments/EdDSARefinement.v
index 484650934..f8e93c6f3 100644
--- a/src/Experiments/EdDSARefinement.v
+++ b/src/Experiments/EdDSARefinement.v
@@ -1,18 +1,19 @@
 Require Import Crypto.Spec.EdDSA Bedrock.Word.
 Require Import Coq.Classes.Morphisms.
 Require Import Crypto.Algebra. Import Group ScalarMult.
-Require Import Util.Decidable Util.Option Util.Tactics.
-Require Import Omega.
+Require Import Crypto.Util.Decidable Crypto.Util.Option Crypto.Util.Tactics.
+Require Import Coq.omega.Omega.
+Require Import Crypto.Util.Notations.
 
 Module Import NotationsFor8485.
   Import NPeano Nat.
-  Infix "mod" := modulo (at level 40).
+  Infix "mod" := modulo.
 End NotationsFor8485.
 
 Section EdDSA.
   Context `{prm:EdDSA}.
   Context {eq_dec:DecidableRel Eeq}.
-  Local Infix "==" := Eeq (at level 69, no associativity).
+  Local Infix "==" := Eeq.
   Local Notation valid := (@valid E Eeq Eadd EscalarMult b H l B Eenc Senc).
   Local Infix "*" := EscalarMult. Local Infix "+" := Eadd. Local Infix "++" := combine.
   Local Notation "P - Q" := (P + Eopp Q).
diff --git a/src/ModularArithmetic/ModularBaseSystemList.v b/src/ModularArithmetic/ModularBaseSystemList.v
index b46429fcc..c556427b9 100644
--- a/src/ModularArithmetic/ModularBaseSystemList.v
+++ b/src/ModularArithmetic/ModularBaseSystemList.v
@@ -14,7 +14,7 @@ Local Open Scope Z_scope.
 Section Defs.
   Context `{prm :PseudoMersenneBaseParams} (modulus_multiple : digits).
   Local Notation base := (base_from_limb_widths limb_widths).
-  Local Notation "u [ i ]" := (nth_default 0 u i) (at level 40).
+  Local Notation "u [ i ]" := (nth_default 0 u i).
 
   Definition decode (us : digits) : F modulus := ZToField (BaseSystem.decode base us).
 
@@ -68,4 +68,4 @@ Section Defs.
        Otherwise, it's all zeroes, and the subtractions do nothing. *)
      map2 (fun x y => x - y) us (map (Z.land and_term) modulus_digits).
 
-End Defs.
\ No newline at end of file
+End Defs.
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index a1370d33e..d740cca17 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -208,7 +208,7 @@ Section PseudoMersenneProofs.
         split; [ intuition | ].
         destruct Hcarry_done as [Hnth_nonneg Hshiftr_0].
         apply Z.shiftr_eq_0_iff in Hshiftr_0.
-        destruct Hshiftr_0 as [nth_0 | []]; [ rewrite nth_0; zero_bounds | ].
+        destruct Hshiftr_0 as [nth_0 | [] ]; [ rewrite nth_0; zero_bounds | ].
         apply Z.log2_lt_pow2; auto.
       - rewrite nth_default_out_of_bounds by omega.
         split; zero_bounds.
@@ -482,8 +482,8 @@ Section CanonicalizationProofs.
   Qed.
   Hint Rewrite @nth_default_carry using (omega || distr_length; omega) : push_nth_default.
 
-  Local Notation "u '[' i ']' "  := (nth_default 0 u i) (at level 30).
-  Local Notation "u '{{' i '}}' "  := (carry_sequence (make_chain i) u) (at level 30).
+  Local Notation "u [ i ]"  := (nth_default 0 u i).
+  Local Notation "u {{ i }}"  := (carry_sequence (make_chain i) u) (at level 30). (* Can't rely on [Reserved Notation]: https://coq.inria.fr/bugs/show_bug.cgi?id=4970 *)
 
   Lemma bound_during_first_loop : forall i n us,
     length us = length limb_widths ->
diff --git a/src/Util/Notations.v b/src/Util/Notations.v
index 3aa80406b..b23fe37ac 100644
--- a/src/Util/Notations.v
+++ b/src/Util/Notations.v
@@ -17,8 +17,36 @@ Reserved Notation "x ^ 2" (at level 30, format "x ^ 2").
 Reserved Notation "x ^ 3" (at level 30, format "x ^ 3").
 Reserved Infix "mod" (at level 40, no associativity).
 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).
 Reserved Infix "∣" (at level 50).
 Reserved Infix "~=" (at level 70).
+Reserved Infix "==" (at level 70, no associativity).
+Reserved Notation "a !== b" (at level 70, no associativity).
+Reserved Notation "$$ v" (at level 40).
+Reserved Notation "% A" (at level 20, right associativity).
+Reserved Notation "$ A" (at level 20, right associativity).
+Reserved Notation "A :[ B ]:" (at level 20, right associativity).
+Reserved Notation "# A" (at level 20, right associativity).
+Reserved Notation "A :+: B" (at level 60, right associativity).
+Reserved Notation "A :+c: B" (at level 60, right associativity).
+Reserved Notation "A :-: B" (at level 60, right associativity).
+Reserved Notation "A :&: B" (at level 45, right associativity).
+Reserved Notation "A :^: B" (at level 45, right associativity).
+Reserved Notation "A :>>: B" (at level 60, right associativity).
+Reserved Notation "A :<<: B" (at level 60, right associativity).
+Reserved Notation "A :*: B" (at level 55, right associativity).
+(*Reserved Notation "O :( A , B ): :?: L ::: R" (at level 70, right associativity).*) (* breaks everything *)
+Reserved Notation "F :**: e" (at level 70, right associativity).
+Reserved Notation "E :->: F" (at level 70, right associativity).
+Reserved Notation "A :|: B" (at level 65, left associativity).
+Reserved Notation "n ::: A :():" (at level 65, left associativity).
+Reserved Notation "& x" (at level 30).
+Reserved Notation "** x" (at level 30).
+Reserved Notation "A <- X ; B" (at level 70, right associativity).
+Reserved Notation "'plet' x := y 'in' z" (at level 60).
+Reserved Notation "u [ i ]" (at level 30).
+Reserved Notation "v [[ i ]]" (at level 30).
+Reserved Notation "u {{ i }}" (at level 30).
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 939ada461..ab844e9ad 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -214,7 +214,7 @@ Module Z.
     rewrite Z.mul_comm in c_id.
     apply Zdivide_intro in c_id.
     apply prime_divisors in c_id; auto.
-    destruct c_id; [omega | destruct H; [omega | destruct H; auto]].
+    destruct c_id; [omega | destruct H; [omega | destruct H; auto] ].
     pose proof (prime_ge_2 p prime_p); omega.
   Qed.
 
@@ -828,9 +828,9 @@ Module Z.
     | _ => lia
     | _ => progress subst
     | [ H : ?n * ?m < 0 |- _ ]
-      => apply (proj1 (Z.lt_mul_0 n m)) in H; destruct H as [[??]|[??]]
+      => apply (proj1 (Z.lt_mul_0 n m)) in H; destruct H as [ [??]|[??] ]
     | [ H : ?n / ?m < 0 |- _ ]
-      => apply (proj1 (lt_div_0 n m)) in H; destruct H as [[[??]|[??]]?]
+      => apply (proj1 (lt_div_0 n m)) in H; destruct H as [ [ [??]|[??] ] ? ]
     | [ H : (?x^?y) <= ?n < _, H' : ?n < 0 |- _ ]
       => assert (0 <= x^y) by zero_bounds; lia
     | [ H : (?x^?y) < 0 |- _ ]
@@ -841,7 +841,7 @@ Module Z.
          assert (x^y = 0) by lia;
          clear H H'
     | [ H : _^_ = 0 |- _ ]
-      => apply Z.pow_eq_0_iff in H; destruct H as [?|[??]]
+      => apply Z.pow_eq_0_iff in H; destruct H as [ ?|[??] ]
     | [ H : 0 <= ?x, H' : ?x - 1 < 0 |- _ ]
       => assert (x = 0) by lia; clear H H'
     | [ |- ?x <= ?y ] => is_evar x; reflexivity
diff --git a/src/WeierstrassCurve/Pre.v b/src/WeierstrassCurve/Pre.v
index b140e95b5..c51c82e89 100644
--- a/src/WeierstrassCurve/Pre.v
+++ b/src/WeierstrassCurve/Pre.v
@@ -50,7 +50,7 @@ Section Pre.
   Lemma unifiedAdd'_onCurve : forall P1 P2,
     onCurve P1 -> onCurve P2 -> onCurve (unifiedAdd' P1 P2).
   Proof.
-    unfold onCurve, unifiedAdd'; intros [[x1 y1]|] [[x2 y2]|] H1 H2;
+    unfold onCurve, unifiedAdd'; intros [ [x1 y1]|] [ [x2 y2]|] H1 H2;
       break_match; trivial; setoid_subst_rel eq; only_two_square_roots; super_nsatz.
   Qed.
 End Pre.