A (significant) simplification in printing notations with recursive binders.

For historical reasons (this was one of the first examples of
notations with binders), there was a special treatment for notations
whose right-hand side had the form "forall x, P" or "fun x => P". Not
only this is not necessary, but this prevents notations binding to
expressions such as "forall x, x>0 -> P" to be used in printing.

We let the general case absorb this particular case.

We add the integration of "let x:=c in ..." in the middle of a
notation with recursive binders as part of the binder list, reprinting
it "(x:=c)" (this was formerly the case only for the above particular
case).

Note that integrating "let" in sequence of binders is stil not the
case for the regular "forall"/"fun". Should we?

0 files changed, 0 insertions, 0 deletions