From 6d0d4997982735fbfa366e52770df878a71bc906 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Fri, 5 Jun 2020 13:28:17 +0200
Subject: [PATCH] Use right lemma in automation

---
 theories/logrel/subtyping_rules.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/logrel/subtyping_rules.v b/theories/logrel/subtyping_rules.v
index c52b383..5badbfd 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.
-- 
GitLab