Fixing/improving notations with recursive patterns.

- The "terminator" of a recursive notation is now interpreted in the
  environment in which it occurs rather than the environment at the
  beginning of the recursive patterns.

  Note that due to a tolerance in checking unbound variables of
  notations, a variable unbound in the environment was still working
  ok as long as no user-given variable was shadowing a private
  variable of the notation - see the "exists_mixed" example in
  test-suite.

  Conversely, in a notation such as:

    Notation "!! x .. y # A #" :=
      ((forall x, True), .. ((forall y, True), A) ..)
      (at level 200, x binder).
    Check !! a b # a=b #.

  The unbound "a" was detected only at pretyping and not as expected
  at internalizing time, due to "a=b" interpreted in context
  containing a and b.

- Similarly, each binder is now interpreted in the environment in
  which it occurs rather than as if the sequence of binders was
  dependent from the left to the right (such a dependency was ok for
  "forall" or "exists" but not in general).

  For instance, in:

    Notation "!! x .. y # A #" :=
      ((forall x, True), .. ((forall y, True), A) ..)
      (at level 200, x binder).
    Check !! (a:nat) (b:a=a) # True #.

  The illegal dependency of the type of b in a was detected only at
  pretyping time.

- If a let-in occurs in the sequence of binders of a notation with a
  recursive pattern, it is now inserted in between the occurrences of
  the iterator rather than glued with the forall/fun of the iterator.
  For instance, in:

    Notation "'exists_true' x .. y , P" :=
      (exists x, True /\ .. (exists y, True /\ P) ..)
      (at level 200, x binder).
    Check exists_true '(x,y) (u:=0), x=y.

  We now get

    exists '(x, y), True /\ (let u := 0 in True /\ x = y)

  while we had before the let-in breaking the repeated pattern:

    exists '(x, y), (let u := 0 in True /\ x = y)

  This is more compositional, and, in particular, the printer algorithm
  now recognizes the pattern which is otherwise broken.

0 files changed, 0 insertions, 0 deletions