From f81b0ff3fee44b543610539d2cf3e089968f388f Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 12 Jul 2016 11:00:46 +0200
Subject: [PATCH] Heap_lang notation for inequality.

---
 heap_lang/notation.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/heap_lang/notation.v b/heap_lang/notation.v
index faed72775..4a33e5a6b 100644
--- a/heap_lang/notation.v
+++ b/heap_lang/notation.v
@@ -58,6 +58,7 @@ Notation "e1 - e2" := (BinOp MinusOp e1%E e2%E)
 Notation "e1 ≤ e2" := (BinOp LeOp e1%E e2%E) (at level 70) : expr_scope.
 Notation "e1 < e2" := (BinOp LtOp e1%E e2%E) (at level 70) : expr_scope.
 Notation "e1 = e2" := (BinOp EqOp e1%E e2%E) (at level 70) : expr_scope.
+Notation "e1 ≠ e2" := (UnOp NegOp (BinOp EqOp e1%E e2%E)) (at level 70) : expr_scope.
 Notation "~ e" := (UnOp NegOp e%E) (at level 75, right associativity) : expr_scope.
 (* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
 Notation "e1 <- e2" := (Store e1%E e2%E) (at level 80) : expr_scope.
-- 
GitLab