Fixing the essence of naming bug #3204: use same strategy for naming

cases pattern variables than for naming forall/fun binders (but still
avoiding constructor names).

Note in passing: such as it is implemented, the general strategy is in
O(n²) in the number of nested binders, because, when computing the
name for each 'fun x => c" (or forall, or a pattern name), the names
from the outside c and visibly occurring in c are computed.

0 files changed, 0 insertions, 0 deletions