From c6c878843a2ed6eaca06589d566509544bc864c3 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 15 Feb 2018 16:20:06 +0100
Subject: [PATCH] Also remove the [cbv zeta].
---
theories/proofmode/tactics.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 186a92944..9e06f66fa 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -628,7 +628,7 @@ Tactic Notation "iIntoValid" open_constr(t) :=
let e := fresh in evar (e:id T);
let e' := eval unfold e in e in clear e; go (t e')
| _ =>
- let tT' := eval cbv zeta in tT in eapply (as_valid_1 tT');
+ eapply (as_valid_1 tT);
(* Doing [apply _] here fails because that will try to solve all evars
whose type is a typeclass, in dependency order (according to Matthieu).
If one fails, it aborts. However, we rely on progress on the main goal
--
GitLab