Merge pull request #29 from SkySkimmer/clenv-unify-cv-pb #135
Annotations
10 warnings
|
build:
theories/Automation/Hints.v#L147
Notation Ropp_minus_distr' is deprecated since 8.19.
|
|
build:
theories/Automation/Hints.v#L171
Notation Ropp_div is deprecated since 8.19. Use Rdiv_opp_l.
|
|
build:
theories/Libs/Analysis.v#L20
Notation "_ is an _accumulation point_" was already used.
|
|
build:
theories/Libs/Analysis.v#L20
Notation "_ is an accumulation point" was already used.
|
|
build:
theories/Libs/Analysis.v#L20
Notation "_ is an _isolated point_" was already used.
|
|
build:
theories/Libs/Analysis.v#L20
Notation "_ is an isolated point" was already used.
|
|
build:
theories/Libs/Analysis.v#L20
Notation "_limit_ of _ in _ is _" was already used.
|
|
build:
theories/Libs/Analysis.v#L20
Notation "limit of _ in _ is _" was already used.
|
|
build:
theories/Libs/Analysis.v#L20
Notation "_ is _continuous_ in _" was already used.
|
|
build:
theories/Libs/Analysis.v#L20
Notation "_ is continuous in _" was already used.
|