The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

When reading the reference manual, I discovered a line [Parameter Inline(10) t : Type.] in http://coq.inria.fr/library/Coq.Structures.Equalities.html#.  I found the section on [Inline] to be incomprehensible; it says

 

     3. assumption_keyword Inline assums

The instance of this assumption will be automatically expanded at functor application, except when this functor application is prefixed by a ! annotation.

What is the purpose of [Inline], what's an example where it matters, and what does the "(10)" do?

Thanks,

Jason