From e35486ca3a6a5f08d6de85905cd277d813d7891e Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Mon, 14 Feb 2022 12:23:50 +0100
Subject: [PATCH] Remove possibly costly call to auto in From/IntoTExist.
---
theories/util_instances.v | 7 +++++--
1 file changed, 5 insertions(+), 2 deletions(-)
diff --git a/theories/util_instances.v b/theories/util_instances.v
index a75c284c..f7cbbb0a 100644
--- a/theories/util_instances.v
+++ b/theories/util_instances.v
@@ -724,12 +724,15 @@ Global Hint Extern 0 (FromExistCareful ?L ?R) =>
end in
solve : typeclass_instances.
+Lemma exactly_entails {PROP : bi} (P : PROP) : P ⊢ P.
+Proof. done. Qed.
+
Global Hint Extern 4 (FromTExistDirect (bi_exist ?input_fun) ?TT ?Q') =>
match get_biexist_function_and_tele input_fun with
| (?output_fun, ?telescope) =>
unify TT telescope;
unify output_fun Q';
- by rewrite /FromTExistDirect /FromTExist
+ refine (exactly_entails _)
end : typeclass_instances.
Global Hint Extern 4 (IntoTExistExact (bi_exist ?input_fun) ?TT ?Q') =>
@@ -737,7 +740,7 @@ Global Hint Extern 4 (IntoTExistExact (bi_exist ?input_fun) ?TT ?Q') =>
| (?output_fun, ?telescope) =>
unify TT telescope;
unify output_fun Q';
- by rewrite /IntoTExistExact /IntoTExist
+ refine (exactly_entails _)
end : typeclass_instances.
Global Hint Extern 4 (FindInContext ?Δ ?PTC ?k ?r ?R) =>
--
GitLab