The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

There is no simple way. Some people have started to pack their notations in submodules to that effect, but it doesn't work very well.

This sort of features has been on the todo list for years. But more pressing matters usually take over.

On 17 May 2013 06:19, Gregory Malecha <gmalecha AT cs.harvard.edu> wrote:

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/