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

...olable proof terms. As discussed in #454.
Why do we have the convention? We have `Locate` .

On Mon, Sep 8, 2014 at 7:03 PM, Jason Gross <notifications@github.com>
wrote:

> In contrib/HoTTBook.v:
>
> > @@ -69,7 +69,7 @@ Definition Book_2_1_1 := @HoTT.Overture.inverse.
> >  (* ================================================== lem:concat *)
> >  (** Lemma 2.1.2 *)
> >
> > -Definition Book_2_1_2 := @HoTT.Overture.concat.
> > +Definition Book_2_1_2 := @transitive_paths.
>
> I think, by convention, this should be @HoTT.Overture.transitive_paths,
> not @transitive_paths.
>
> —
> Reply to this email directly or view it on GitHub
> <https://github.com/HoTT/HoTT/pull/459/files#r17251285>.
>