The Coq mailing list

[Ralf Jung <jung AT mpi-sws.org>]

Hi,

> Is there anything like an Arguments command that will allow only
> specifically chosen implicits to print?  I know I can do Arguments :
> clear implicits, but I don't want parsing impacted, and only temporarily
> want printing impacted.  Set Printing Implicit is a blunt instrument. 
> The Defensive modifier is also too blunt.  I'm hoping maybe there is an
> undocumented Argument command that already does this...
> 
> The use case is: a particular function where the implicits work very
> well parsing-wise, but often become confusing during proving, as when
> one sees a conclusion like "foo x = foo x", but reflexivity fails due to
> differences in the implicits (even f_equal fails to progress).  And
> there are many other implicits in other functions around working very
> nicely to make the goals easy to read, so using Set Printing Implicit,
> Defenisve or not, is not a good idea.  In such a case, it would be nice
> to do something like "Arguments foo : {no}print implicits" to turn them
> on and off, so that foo would always print as @foo.

One thing you could do is not have that argument implicit, and then
define a parsing only notation that adds the underscore to trigger
inference. Like

Definition foo (n : nat) := n.
Notation foo' := (foo _) (only parsing).

This means you have to use foo' when writing but will see foo in the
proof state; but other than that, I think the implicits should behave
the way you want.

Kind regards,
Ralf