Skip to content
Snippets Groups Projects
Commit 5e3705ea authored by Ike Mulder's avatar Ike Mulder
Browse files

Apparently 'rewrite /term' is way slower than 'unfold term'.

parent 07415805
No related branches found
No related tags found
No related merge requests found
Pipeline #62059 passed
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 1 deletion
theories/tele_utils.v
+ 1
− 1
View file @ 5e3705ea
......@@ -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.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment