coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] The implicit-argument-ness of type classes

From: Jason Gross <jasongross9 AT gmail.com>
To: Matthieu Sozeau <matthieu.sozeau AT gmail.com>
Cc: Michiel Helvensteijn <mhelvens AT gmail.com>, Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] The implicit-argument-ness of type classes
Date: Sun, 21 Jul 2013 19:07:09 -0400

> - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -
> 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 think [Arguments elements : clear implicits.] might do what you want.

-Jason

[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