diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index a6c6da9700887bf8007a0eee636d2da61465970e..15fb921b797d30c6ce9d97e8e00e6655be2e297f 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -1027,13 +1027,7 @@ Tactic Notation "iPoseProofCore" open_constr(lem)
     end in
   lazymatch type of t with
   | ident => iPoseProofCoreHyp t as Htmp; spec_tac (); [..|tac Htmp]
-  | _ =>
-     lazymatch eval compute in lazy_tc with
-     | true =>
-        iPoseProofCoreLem t as Htmp before_tc (spec_tac (); [..|tac Htmp])
-     | false =>
-        iPoseProofCoreLem t as Htmp before_tc (spec_tac (); [..|tac Htmp])
-     end
+  | _ => iPoseProofCoreLem t as Htmp before_tc (spec_tac (); [..|tac Htmp])
   end.
 
 (** * The apply tactic *)