diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 186a9294402c94d72f63dd970dd304377710da87..9e06f66fa578b78d4890db01ba6c826f802ab3ea 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