From aaa4f987c56474bd1689c2ea638c44b57b56e4ad Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 26 Sep 2017 22:52:10 +0200
Subject: [PATCH] Make `closed_dec` transparent by using `Defined`.
---
theories/heap_lang/lang.v | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/theories/heap_lang/lang.v b/theories/heap_lang/lang.v
index bb3a90d30..df0fae3cf 100644
--- a/theories/heap_lang/lang.v
+++ b/theories/heap_lang/lang.v
@@ -75,10 +75,10 @@ Fixpoint is_closed (X : list string) (e : expr) : bool :=
end.
Class Closed (X : list string) (e : expr) := closed : is_closed X e.
-Instance closed_proof_irrel env e : ProofIrrel (Closed env e).
-Proof. rewrite /Closed. apply _. Qed.
-Instance closed_decision env e : Decision (Closed env e).
+Instance closed_proof_irrel X e : ProofIrrel (Closed X e).
Proof. rewrite /Closed. apply _. Qed.
+Instance closed_dec X e : Decision (Closed X e).
+Proof. rewrite /Closed. apply _. Defined.
Inductive val :=
| RecV (f x : binder) (e : expr) `{!Closed (f :b: x :b: []) e}
--
GitLab