From 4140073905978b5970959c5ac973936471bad43b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 18 May 2020 13:33:32 +0200
Subject: [PATCH] exhaustive match for lit_is_unboxed

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

diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index 64882ac8f..0df1c4053 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -162,7 +162,7 @@ Definition lit_is_unboxed (l: base_lit) : Prop :=
   (** Disallow comparing (erased) prophecies with (erased) prophecies, by
   considering them boxed. *)
   | LitProphecy _ | LitPoison => False
-  | _ => True
+  | LitInt _ | LitBool _  | LitLoc _ | LitUnit => True
   end.
 Definition val_is_unboxed (v : val) : Prop :=
   match v with
-- 
GitLab