Aggregate all level specifications not in Spec/*

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

1 files changed, 20 insertions, 0 deletions

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).