Yes, I meant something like that. I am somewhat surprised refine is so slow.
Ssreflect uses something similar.


On Sun, Apr 27, 2014 at 10:08 PM, Jason Gross <notifications@github.com>wrote:

> In theories/categories/FunctorCategory/Morphisms.v:
>
> > @@ -34,6 +34,10 @@ Proof.
> >  Defined.
> >
> >  Hint Immediate isisomorphism_components_of : typeclass_instances.
> > +(** When one of the functors is the identity functor, we fail to match correctly, because [apply] is stupid.  So we do its work for it. *)
>
> Quoting @spitters <https://github.com/spitters> on e39ea93<https://github.com/HoTT/HoTT/commit/e39ea93064e9be276300fc580e2e8387c947094b>(on the unified diff, so that it sticks around even if I rebase)
>
> Doesn't refine do this for you ?
> There is a special [rapply] in coqorico for this.
>
> I replied:
> refine works, but is slower (in a totally out-of-context comparison, it
> slows a tactic down from 2.9s to 3.5s). The only rapply I could find is
> at http://www.cis.upenn.edu/~bcpierce/sf/LibTactics.html#lab828.
>
> —
> Reply to this email directly or view it on GitHub<https://github.com/HoTT/HoTT/pull/384/files#r12031068>
> .
>