Printing notations: Cleaning in anticipation of fixing #4592.

- Making a clear distinction between expressions of the notation which
  are associated to binding variables only (as in `Notation "'lam' x ,
  P" := (fun x => P)" or `Notation "'exists2' x : t , p & q" := (ex2
  (fun x:t => p) (fun x:t => q))') and those which are associated to
  at list one subterm (e.g. `Notation "x .+1" := (S x)' but also
  "Notation "{# x | P }" := (ex2 _ (fun y => x = F y) (fun x => P))'
  as in #4592). The former have type NtnTypeOnlyBinder.
- Thus avoiding in particular encoding too early Anonymous as GHole
  and "Name id" as "GVar id".

There is a non-trivial alpha-conversion work to do to get #4592
working. See comments in Notation_ops.add_env.

0 files changed, 0 insertions, 0 deletions