The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

> But I still think it is weird that
> these other declarations without proofs automagically become instances
> of Existing Class types, while definitions - declarations with proofs -
> don't.  I can understand how hypotheses in a local context of a proof
> benefit from becoming instances automatically - but in those command
> cases, one always has the opportunity to explicitly add them with
> Existing Instance, so the automatic aspect there is just a small
> convenience, right?

We are certainly relying on this in our Coq development, where we will
often have things like

Section Foo.
  Context (f: T1 -> T2) `{Proper (equiv ==> equiv) f}.

  (* Now rewriting with equivalences below [f] just works.
End Foo.

Having to give a name to the [Proper] instance, and then doing an
explicit "Local Existing Instance", sounds rather cumbersome.

Kind regards,
Ralf