aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Util/Notations.v2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Util/Notations.v b/src/Util/Notations.v
index b23fe37ac..222f63498 100644
--- a/src/Util/Notations.v
+++ b/src/Util/Notations.v
@@ -24,7 +24,9 @@ Reserved Infix "&" (at level 50).
Reserved Infix "∣" (at level 50).
Reserved Infix "~=" (at level 70).
Reserved Infix "==" (at level 70, no associativity).
+Reserved Infix "≡" (at level 70, no associativity).
Reserved Notation "a !== b" (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).