fix for Coq v8.18 compatibility #136
YoungchanChoAnnotations
3 errors and 30 warnings
|
build (8.12, default):
RealAux.v#L27
This command does not support this attribute: export.
|
|
build (8.13, default):
RealAux.v#L27
This command does not support this attribute: export.
|
|
build (dev, default):
Matrix.v#L309
The reference lt_S_n was not found in the current environment.
|
|
build (dev, default):
Prelim.v#L378
Notation app_nil_end is deprecated since 8.18.
|
|
build (dev, default):
Prelim.v#L378
Notation app_nil_end is deprecated since 8.18.
|
|
build (dev, default):
Prelim.v#L378
Notation app_nil_end is deprecated since 8.18.
|
|
build (dev, default):
Summation.v#L535
Notation Nat.add_mod is deprecated since 8.17.
|
|
build (dev, default):
Summation.v#L535
Notation Nat.add_mod is deprecated since 8.17.
|
|
build (dev, default):
Summation.v#L535
Notation Nat.add_mod is deprecated since 8.17.
|
|
build (dev, default):
Summation.v#L536
Notation Nat.mod_mul is deprecated since 8.17.
|
|
build (dev, default):
Summation.v#L536
Notation Nat.mod_mul is deprecated since 8.17.
|
|
build (dev, default):
Summation.v#L536
Notation Nat.mod_mul is deprecated since 8.17.
|
|
build (dev, default):
Summation.v#L560
Notation Nat.mod_add is deprecated since 8.17.
|
|
build (8.17, default):
Summation.v#L535
Notation Nat.add_mod is deprecated since 8.17.
|
|
build (8.17, default):
Summation.v#L535
Notation Nat.add_mod is deprecated since 8.17.
|
|
build (8.17, default):
Summation.v#L535
Notation Nat.add_mod is deprecated since 8.17.
|
|
build (8.17, default):
Summation.v#L536
Notation Nat.mod_mul is deprecated since 8.17.
|
|
build (8.17, default):
Summation.v#L536
Notation Nat.mod_mul is deprecated since 8.17.
|
|
build (8.17, default):
Summation.v#L536
Notation Nat.mod_mul is deprecated since 8.17.
|
|
build (8.17, default):
Summation.v#L560
Notation Nat.mod_add is deprecated since 8.17.
|
|
build (8.17, default):
Summation.v#L560
Notation Nat.mod_add is deprecated since 8.17.
|
|
build (8.17, default):
Summation.v#L560
Notation Nat.mod_add is deprecated since 8.17.
|
|
build (8.17, default):
Summation.v#L560
Notation Nat.mod_add is deprecated since 8.17.
|
|
build (8.16, default):
RealAux.v#L41
Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
|
|
build (8.16, default):
RealAux.v#L41
Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
|
|
build (8.16, default):
RealAux.v#L41
Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
|
|
build (8.16, default):
RealAux.v#L41
Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
|
|
build (8.16, default):
RealAux.v#L41
Notation Rinv_mult_distr is deprecated since 8.16. Use Rinv_mult.
|
|
build (8.16, default):
Polar.v#L59
Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
|
|
build (8.16, default):
Polar.v#L59
Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
|
|
build (8.16, default):
Polar.v#L59
Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
|
|
build (8.16, default):
Polar.v#L59
Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
|
|
build (8.16, default):
Polar.v#L81
Notation Rabs_Rinv is deprecated since 8.16. Use Rabs_inv.
|