The Coq mailing list

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

Dear Valentin,

> According to the reference manual:
> "Notations do not survive the end of sections."
> 
> I would like to understand whether a) this is a wanted feature b) this is a
> constraint or c) a choice of the current implementation, or d) this is due 
> to
> some theoretical issue with trying to make them survive.

One certainly would like notations to sometimes survive section. If I
did not implement it, it is because I did not see what clear strategy
to follow in adapting the notations to the new expression it refers
to. Thinking to it again now, one could use the strategy that all
extra arguments of the constants involved in the notation are replaced
by "_". For instance, that would be fine for an example such as:

Section projection.
  Variables A B : Type.
  Definition fst `((x,y):A*B) := x.
  Notation "p .1" := (fst p).
End projection.
(* One would redefine the notation to
Notation "p .1" := (fst _ _ p).
*)

But, then, is it reasonable to do that systematically without even
checking that the added "_" are inferable? Shall we then couple this
generalization with a test that the arguments are inferable? Or with a
test that the arguments are declared as implicit? Or really let it
entirely to the responsability of the user that the resulting notation
makes sense?

It is this kind of questions that I was not able to answer and which
led me to not let notations survive sections.

But you're completely right, one could do better, and we can discuss
further if you are interested.

Hugo