The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Guillaume, Maxime,

I thought about the implicit argument definitions in the standard library 
once more and came to the conclusion that (except for type class cases as 
mentioned by Ralf Jung) it might make more sense to switch to maximally 
inserted definitions right away and provide a compatibility layer with 
argument declarations for code which needs it. Something like:

Inductive sig {A:Type} (P:A -> Prop) : Type :=
    exist : forall x:A, P x -> sig P.

And in a separate compatibility file only used by legacy code which requires 
it:

Arguments sig [A] P.
Arguments exist [A] P.

So for removing "Set Implicit Arguments" the [] syntax suggested by Maxime 
wouldn't be required, but Ralf's argument around type class arguments is 
anyway much stronger.

What do you think about such a compatibility layer, and a legacy 
compatibility layer for the standard library in general? As far as I can tell 
this is already done in some places but not always nicely documented and 
sometimes not in separate files.

Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928