The Coq mailing list

[Chris Dams <chris.dams.nl AT gmail.com>]

Hello Perce,

Thank you for your response. It is not actually this easy, though. Note that the definition of gt is also inside the concrete module and not in the signature. I do not want to export gt because it would conflict with gt of the natural numbers. I guess, I could just move gt to the signature, but for the moment I have now just redeclared my notations outside of the module again. Not particularly pretty but it works.

Regards,

Chris