fix for Coq v8.18 compatibility #139
YoungchanChoAnnotations
5 errors and 40 warnings
|
build (8.13, default):
RealAux.v#L27
This command does not support this attribute: export.
|
|
build (8.12, default):
RealAux.v#L27
This command does not support this attribute: export.
|
|
build (dev, default):
Matrix.v#L1198
In environment
|
|
build (8.15, default):
DiscreteProb.v#L1507
The reference Arith_prebase.mult_O_le_stt was not found in the current
|
|
build (8.14, default):
DiscreteProb.v#L1507
The reference Arith_prebase.mult_O_le_stt was not found in the current
|
|
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.18, default):
Prelim.v#L378
Notation app_nil_end is deprecated since 8.18.
|
|
build (8.18, default):
Prelim.v#L378
Notation app_nil_end is deprecated since 8.18.
|
|
build (8.18, default):
Prelim.v#L378
Notation app_nil_end is deprecated since 8.18.
|
|
build (8.18, default):
Summation.v#L535
Notation Nat.add_mod is deprecated since 8.17.
|
|
build (8.18, default):
Summation.v#L535
Notation Nat.add_mod is deprecated since 8.17.
|
|
build (8.18, default):
Summation.v#L535
Notation Nat.add_mod is deprecated since 8.17.
|
|
build (8.18, default):
Summation.v#L536
Notation Nat.mod_mul is deprecated since 8.17.
|
|
build (8.18, default):
Summation.v#L536
Notation Nat.mod_mul is deprecated since 8.17.
|
|
build (8.18, default):
Summation.v#L536
Notation Nat.mod_mul is deprecated since 8.17.
|
|
build (8.18, 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.
|