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

...olable proof terms. As discussed in #454.
About simpl vs cbn:
simpl vs cbn Decision to expect the new cbn to replace simpl (with a flag
to restore the old behavior of the name "simpl"). Tentative syntax will be
"simpl delta_flag contextually_flag" with "delta_flag" being [cst1 ...
cstn] or -[cst1 ... cstn] and contextually_flag being "cst" or "cst at
occs".

http://coq.inria.fr/cocorico/CoqDevelopment/CoqWG20140905


On Sat, Sep 6, 2014 at 12:54 AM, 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.
>
> What are simpl @fst and simpl -[foo] supposed to do?
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/459/files#r17202768>.
>