coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] The implicit-argument-ness of type classes
- Date: Mon, 22 Jul 2013 01:10:49 +0200
On 07/22/2013 01:03 AM, Matthieu Sozeau wrote:
Anyway, I actually like it... some of the time.That's unfortunate, maybe a bug? You could try the [Implict Arguments
>
> 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
*)
> - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
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
- [Coq-Club] The implicit-argument-ness of type classes, Michiel Helvensteijn, 07/22/2013
- Re: [Coq-Club] The implicit-argument-ness of type classes, Matthieu Sozeau, 07/22/2013
- Re: [Coq-Club] The implicit-argument-ness of type classes, Jason Gross, 07/22/2013
- Re: [Coq-Club] The implicit-argument-ness of type classes, Robbert Krebbers, 07/22/2013
- Re: [Coq-Club] The implicit-argument-ness of type classes, Michiel Helvensteijn, 07/22/2013
- Re: [Coq-Club] The implicit-argument-ness of type classes, Matthieu Sozeau, 07/22/2013
- Re: [Coq-Club] The implicit-argument-ness of type classes, Michiel Helvensteijn, 07/22/2013
- Re: [Coq-Club] The implicit-argument-ness of type classes, Matthieu Sozeau, 07/22/2013
- Re: [Coq-Club] The implicit-argument-ness of type classes, Matthieu Sozeau, 07/22/2013
Archive powered by MHonArc 2.6.18.