The Coq mailing list

[Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>]

Hi,
Le 17 mai 2013 à 17:15, CJ Bell 
<cbell AT CS.Princeton.EDU>
 a écrit :

>> 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?
I don't know what Arnaud has in mind and I do like this approach.
In fact, my point of view is a bit different, I think module shouldn't be 
"Import"ed. But you need to import notations in order to use them. That's why 
I've made a special module for things you want to import in 
Coq.Vectors.Vectors.

Anyway, I see an annoying point : Using notations in the module where you 
define stuff you make notations for asks for defining notations twice. As you 
can see, notations about vectors are defined twice. Once locally in order to 
be allowed to use [] and :: in VectorDef module but not disturb other modules 
and once in the correct module to make them publicly available.
> 
> 
> Thanks,
> -cj
All the best,
Pierre B.