From 324b4863d7d4bec1482bc5b03b2e82f05b6b8023 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 6 Mar 2016 00:59:20 +0100
Subject: [PATCH] Comment on FIXME in heap_lang.

---
 heap_lang/lang.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/heap_lang/lang.v b/heap_lang/lang.v
index c8c901961..c127e0e94 100644
--- a/heap_lang/lang.v
+++ b/heap_lang/lang.v
@@ -40,8 +40,8 @@ Qed.
    tactics, Coq would do things in the wrong order. *)
 Class VarBound (x : string) (X : list string) :=
   var_bound : bool_decide (x âˆˆ X).
-(* FIXME shouldn't this have this Hint to only perfom search of x and X
-   are not evars? *)
+(* There is no need to restrict this hint to terms without evars, [vm_compute]
+will fail in case evars are arround. *)
 Hint Extern 0 (VarBound _ _) => vm_compute; exact I : typeclass_instances. 
 
 Instance var_bound_proof_irrel x X : ProofIrrel (VarBound x X).
-- 
GitLab