The Coq mailing list

[Patrick Loiseleur <Patrick.Loiseleur AT lri.fr>]

Dans son message du Thursday 4 February, David Nowak a écrit : 
> Hello,
> 
> Usage of «Implicit Arguments» is different from 6.2.2.  Does somenone
> wrote a script to update from 6.2.2 to 6.2.3/4 (h_convert only deals
> with Hint and Auto) ?
> 
> Thank you.

Support for implicit arguments was improved between 6.2.2 and 6.2.3,
The difference is that when defining an inductive type with some
implicits arguments, you can (and must) use implicit arguments inside
the definition of constructors.

We are very sorry, but there is no automatic tool to update your files.

Regards,

Patrick Loiseleur

-- 
Patrick.Loiseleur AT lri.fr