The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi,

> Op zaterdag 19 maart 2005 10:28, schreef 
> roconnor AT theorem.ca:
> > I am creating a file, but I don't want to export every definition and
> > lemma.  So I create a Section and use Let and Remark on the items I don't
> > want to export.  But I also want to define some Notations.  The Notations
> > don't seems to survive pas the end of my Section.
> >
> > Is there a simple solution to my problem?
> 
> The obvious (but not so elegant) solution is to re-declare your Notations 
> after ending the section.
> 
> Section concat.
> Definition concat:=...
> Notation "a ++ b" := concat a b.
> End concat.
> Notation "a ++ b" := concat a b.

  Ending a section generalises the objects of the section
relatively to the variables and local definitions of the section.

  In general, there is no canonical way to "generalise" a notation,
that's why they are thrown away at section closing time.

  Hugo Herbelin