coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Export Without Notation

From: CJ Bell <cbell AT CS.Princeton.EDU>
To: Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>
Cc: Gregory Malecha <gmalecha AT cs.harvard.edu>, Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Export Without Notation
Date: Fri, 17 May 2013 11:15:57 -0400

> Some people have started to pack their notations in submodules to that
> effect, but it doesn't work very well.

Could you be more specific on this point? What problems would arise if
the standard library adopted this approach?

Thanks,
-cj

[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