Preliminary work before extending support for binders in notations

(binders shall be substitutable by arbitrary cases patterns).

Giving a proper status to the functions unifying different instance of
the same notation variable (up to alpha-renaming).

Note: The a priori change of semantics in "bind_binding_as_term_env"
which now apply renaming from "unify_id" (as it did in
"bind_bindinglist_as_term_env") should not have an effect since, as
the former comment said, this corresponds to a "Anonymous" case which
should not occur, since the term would have to be bound upwards.

0 files changed, 0 insertions, 0 deletions