coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Chris Dams <chris.dams.nl AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] How to use Notations inside of Modules?
- Date: Mon, 29 Dec 2014 14:15:31 +0100
Ah, now I see. The idea is to nest the Notation module inside of the other module. This indeed works and it makes my code a bit cleaner. Many thanks!
- [Coq-Club] How to use Notations inside of Modules?, Chris Dams, 12/25/2014
- RE: [Coq-Club] How to use Notations inside of Modules?, Perce Strop, 12/25/2014
- Re: [Coq-Club] How to use Notations inside of Modules?, Chris Dams, 12/28/2014
- RE: [Coq-Club] How to use Notations inside of Modules?, Perce Strop, 12/28/2014
- Re: [Coq-Club] How to use Notations inside of Modules?, Chris Dams, 12/29/2014
- RE: [Coq-Club] How to use Notations inside of Modules?, Perce Strop, 12/28/2014
- Re: [Coq-Club] How to use Notations inside of Modules?, Chris Dams, 12/28/2014
- RE: [Coq-Club] How to use Notations inside of Modules?, Perce Strop, 12/25/2014
Archive powered by MHonArc 2.6.18.