The Coq mailing list

[Michael Shulman <mshulman AT ucsd.edu>]

Is it possible to declare a hypothesis in a section which will be
automatically *implicitly* generalized upon completion of the section?
In particular, I would like to do this for an instance declaration, so
that

  Section sect.

    Hypothesis A : Type.
    Hypothesis inst : type_class A.

    Theorem thm : B -> C.
    ...

  End sect.

would be equivalent to

  Theorem `{inst : type_class A} : B -> C.

I suppose that I can do this with

  Implicit Arguments thm [[A] [inst]].

(Is that literally the same thing, or is it going to miss out on some
typeclass magic?)  In any case, that is tedious if the section
contains many definitions and theorems.

Mike