aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Notations.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jagro@google.com>2016-06-23 15:52:48 -0700
committerGravatar Jason Gross <jagro@google.com>2016-06-23 15:52:48 -0700
commitc5b008e59cf53e9bd0c2efda8c680b3ffba58569 (patch)
tree98ee674ca7ed627c69d3637be574610492902076 /src/Util/Notations.v
parent93716330e8fcdb1cc69887eced3bdf5cc178f5ae (diff)
Improve some tactics and lemmas
Diffstat (limited to 'src/Util/Notations.v')
-rw-r--r--src/Util/Notations.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Util/Notations.v b/src/Util/Notations.v
index bbeb50092..c3f776766 100644
--- a/src/Util/Notations.v
+++ b/src/Util/Notations.v
@@ -7,6 +7,7 @@
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 70, no associativity).
Reserved Infix ".+" (at level 50).