coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Export Without Notation

From: Gregory Malecha <gmalecha AT cs.harvard.edu>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Export Without Notation
Date: Fri, 17 May 2013 00:19:34 -0400

Hello --

Is there a good way to export a module without its notation? In the standard library, EquivDec is very convenient, but the module overloads the <> notation which is annoying. Is there a way to export the definitions from EquivDec without the notation?

Thank you.

gregory malecha

http://www.people.fas.harvard.edu/~gmalecha/

[Coq-Club] Export Without Notation, Gregory Malecha, 05/17/2013
- Re: [Coq-Club] Export Without Notation, Arnaud Spiwack, 05/17/2013
  - Re: [Coq-Club] Export Without Notation, CJ Bell, 05/17/2013
    - Re: [Coq-Club] Export Without Notation, Pierre Boutillier, 05/17/2013
      - Re: [Coq-Club] Export Without Notation, CJ Bell, 05/17/2013
      - Re: [Coq-Club] Export Without Notation, Jason Gross, 05/17/2013
        
        Re: [Coq-Club] Export Without Notation, CJ Bell, 05/17/2013