From 5f8cdc5f3bac76e8bb0cf3daed05e4b66c9ca684 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Fri, 8 Jan 2016 12:32:33 +0100
Subject: [PATCH] annotate where we have binders
---
channel/heap_lang.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/channel/heap_lang.v b/channel/heap_lang.v
index 9e8d8833b..0cb39a93f 100644
--- a/channel/heap_lang.v
+++ b/channel/heap_lang.v
@@ -57,7 +57,7 @@ Instance Rename_expr : Rename expr. derive. Defined.
Instance Subst_expr : Subst expr. derive. Defined.
Instance SubstLemmas_expr : SubstLemmas expr. derive. Qed.
-Definition Lam (e: expr) := Rec (e.[up ids]).
+Definition Lam (e: {bind expr}) := Rec (e.[up ids]).
Definition LitUnit := Lit tt.
Definition LitTrue := Lit true.
Definition LitFalse := Lit false.
--
GitLab