The Coq mailing list

[Robbert Krebbers <mailinglists AT robbertkrebbers.nl>]

On 07/22/2013 01:03 AM, Matthieu Sozeau wrote:
> > Anyway, I actually like it... some of the time.
> > >
> > >  I'd like to have some better control over it, but it seems to be a
> > >  stubborn feature. For example, I'd like to turn it off for some
> > >  functions, but I can't seem to manage it:
> > >
> > >  - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
> > >  Arguments elements _ _.
> > >  Print Implicit elements. (* Argument DM is implicit and maximally inserted 
> > *)
> > >  - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
> That's unfortunate, maybe a bug? You could try the [Implict Arguments 
> elements []]
> command instead.

I do not think it is a bug. You should use

  Arguments elements : clear implicits.

See also:


http://coq.inria.fr/distrib/current/refman/Reference-Manual004.html#hevea_command67