From 700646bc8b96630ffab3fc48707b0c2298bbcaa9 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 5 Dec 2017 23:27:34 +0100
Subject: [PATCH] Add bitwise negation on integers.

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

diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index d316826c6..45f540ece 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -317,6 +317,7 @@ Definition subst' (mx : binder) (es : expr) : expr → expr :=
 Definition un_op_eval (op : un_op) (v : val) : option val :=
   match op, v with
   | NegOp, LitV (LitBool b) => Some $ LitV $ LitBool (negb b)
+  | NegOp, LitV (LitInt n) => Some $ LitV $ LitInt (Z.lnot n)
   | MinusUnOp, LitV (LitInt n) => Some $ LitV $ LitInt (- n)
   | _, _ => None
   end.
-- 
GitLab