diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index c52b3831cfcb782d834c16eb7fea4fd2b5f2c460..5badbfd13cbf04904db67fbd6df14c1760659ed3 100644
--- a/theories/logrel/subtyping_rules.v
+++ b/theories/logrel/subtyping_rules.v
@@ -511,4 +511,4 @@ Section subtyping_rules.
 End subtyping_rules.
 
 Hint Extern 0 (environments.envs_entails _ (?x <: ?y)) =>
-  first [is_evar x; fail 1 | is_evar y; fail 1|iApply iProto_le_refl] : core.
+  first [is_evar x; fail 1 | is_evar y; fail 1|iApply lty_le_refl] : core.