From e9ecc057647d1a13c2eefda0a66a411a6aa17e35 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Fri, 5 Apr 2019 10:51:16 +0100
Subject: Coq: add missing effectful existential unpacking case

---
 test/coq/pass/unpacking.sail | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)
 create mode 100644 test/coq/pass/unpacking.sail

(limited to 'test/coq')

diff --git a/test/coq/pass/unpacking.sail b/test/coq/pass/unpacking.sail
new file mode 100644
index 00000000..d0143f40
--- /dev/null
+++ b/test/coq/pass/unpacking.sail
@@ -0,0 +1,16 @@
+default Order dec
+
+$include <prelude.sail>
+
+val f : int -> {'n, 'n >= 0. int('n)} effect {rreg}
+val g : int -> {'n, 'n >= 0. int('n)}
+
+val test : unit -> int effect {rreg}
+
+function test() = {
+  let x1 : {'n, 'n >= 0. int('n)} = f(5);
+  let x2 : int = f(6);
+  let y1 : {'n, 'n >= 0. int('n)} = g(7);
+  let y2 : int = g(8);
+  x1 + x2 + y1 + y2
+}
-- 
cgit v1.2.3