From 5e3705ea82f6ae3ce2f730f1d8c12b53425c2aec Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Tue, 15 Feb 2022 11:53:36 +0100
Subject: [PATCH] Apparently 'rewrite /term' is way slower than 'unfold term'.

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

diff --git a/theories/tele_utils.v b/theories/tele_utils.v
index babbd24e..12c961a9 100644
--- a/theories/tele_utils.v
+++ b/theories/tele_utils.v
@@ -1102,7 +1102,7 @@ Class TCTForall {TT : tele} (P : TT → Prop) :=
 .
 
 Global Hint Extern 4 (TCTForall _) =>
-  rewrite /TCTForall; 
+  unfold TCTForall;
   progress cbn [tforall tele_fold tele_bind tele_app TeleConcatType tele_appd_dep];
   intros : typeclass_instances.
 
-- 
GitLab