diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-09-28 15:29:58 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-09-28 16:14:11 +0200 |
| commit | dfadb394640b3d09eb6134b73d0f3e931bd70af1 (patch) | |
| tree | b7f0bba04890b0c905f06829d97d98642168b38f /theories | |
| parent | 8e0f29cb69f06b64d74b18b09fb6a717034f1140 (diff) | |
Warning about similar notations now up to alpha-conversion.
This allows to define on purpose the very same notation in different
files, as currently the notations for *, +, - in Nat.v and Peano.v
(with the first one using variables n and m and the second one using
the default variables used by Infix, namely x and y).
This makes also the "notation-overridden" warning less enigmatic
facing two notations which are the same up to the choice of names.
Diffstat (limited to 'theories')
0 files changed, 0 insertions, 0 deletions