Commit 324b4863 authored by Robbert Krebbers's avatar Robbert Krebbers

Comment on FIXME in heap_lang.

parent 0e48566f
Pipeline #262 passed with stage
......@@ -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).
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment