From b03273836fdf0c2ae1a92f8c0ba6fcdd5722b52d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 31 May 2016 12:20:32 +0200
Subject: [PATCH] Make iFresh more robust in the presence of evars.
---
proofmode/tactics.v | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 119306c55..13331d2ee 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -24,8 +24,10 @@ Ltac iFresh :=
|- of_envs ?Δ ⊢ _ =>
match goal with
| _ => eval vm_compute in (fresh_string_of_set "~" (dom stringset Δ))
- (* [vm_compute fails] if [Δ] contains evars, so fall-back to [cbv] *)
- | _ => eval cbv in (fresh_string_of_set "~" (dom stringset Δ))
+ | _ =>
+ (* [vm_compute fails] if [Δ] contains evars, so fall-back to [cbv] *)
+ let Hs := eval cbv in (dom stringset Δ) in
+ eval vm_compute in (fresh_string_of_set "~" Hs)
end
| _ => constr:"~"
end.
--
GitLab