The Coq mailing list

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

Dear Guillaume,

> What do you have in mind?

You are right, one could keep "Set Implicit Arguments" in a file until all 
implicit arguments are changed to the "explicitly maximally inserted 
implicit" notation. But I think removing "Set Implicit Arguments", use {} for 
all implicit arguments and change this to [] where legacy code requires this 
and then, one by one, replace the [] with {} adjusting the code depending on 
[] looks like a more viable path. Without this "Set Implicit Arguments" will 
probably never go away. Of cause this assumes that there is substantial 
amount of legacy code which won't work with maximally inserted implicit 
arguments.

Btw.: I still wonder where the scope difference comes from.

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