From a0198e0cac509ece542831fe2c62fcab3612b5ca Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 15 Nov 2016 18:16:05 -0500
Subject: Add UnReturn, UnAbs

---
 src/Reflection/Syntax.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v
index 2f99be49c..b70f939ae 100644
--- a/src/Reflection/Syntax.v
+++ b/src/Reflection/Syntax.v
@@ -195,6 +195,16 @@ Section language.
       | Abs {src dst} : (var src -> expr dst) -> expr (Arrow src dst).
       Bind Scope expr_scope with expr.
       Global Coercion Return : exprf >-> expr.
+      Definition UnReturn {t} (e : expr (Tflat t)) : exprf t
+        := match e with
+           | Return _ v => v
+           | Abs _ _ _ => I
+           end.
+      Definition UnAbs {src dst} (e : expr (Arrow src dst)) : var src -> expr dst
+        := match e with
+           | Return _ _ => I
+           | Abs _ _ f => f
+           end.
       (** Sometimes, we want to deal with partially-interpreted
           expressions, things like [prod (exprf A) (exprf B)] rather
           than [exprf (Prod A B)], or like [prod (var A) (var B)] when
-- 
cgit v1.2.3