Using the standard (type class based) transitivity tactic for more contr...

...olable proof terms. As discussed in #454.
simpl is broken. This is precisely the reason cbn has been introduced.
simpl will probably be deprecated.


On Thu, Sep 4, 2014 at 8:18 PM, Mike Shulman <notifications@github.com>
wrote:

> In theories/PathGroupoids.v:
>
> > @@ -440,7 +440,7 @@ Definition concat_A_pp {A B : Type} {f g : A -> B} (p : forall x, f x = g x)
> >    :
> >    (ap f q) @ (p y @ s) = (p x) @ (ap g q @ s).
> >  Proof.
> > -  destruct q, s; simpl.
> > +  destruct q, s; cbn.
>
> I think this is a showstopper, if simpl can't simplify idpath @ idpath.
> Why on earth?
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/459/files#r17132006>.
>