partial fixes tutorial/kvservice/full_proof.v #196
zeldovichAnnotations
21 warnings
|
build-vos (dev):
external/coqutil/src/coqutil/Z/Lia.v#L1
Coq.ZArith.ZArith has been replaced by Stdlib.ZArith.ZArith.
|
|
build-vos (dev):
external/coqutil/src/coqutil/Z/div_mod_to_equations.v#L1
Coq.ZArith.BinInt has been replaced by Stdlib.ZArith.BinInt.
|
|
build-vos (dev):
external/coqutil/src/coqutil/Word/Interface.v#L3
Coq.ZArith.BinIntDef has been replaced by Stdlib.ZArith.BinIntDef.
|
|
build-vos (dev):
external/coqutil/src/coqutil/Word/Interface.v#L3
Coq.ZArith.BinInt has been replaced by Stdlib.ZArith.BinInt.
|
|
build-vos (dev):
external/coqutil/src/coqutil/Z/Lia.v#L2
Coq.micromega.Lia has been replaced by Stdlib.micromega.Lia.
|
|
build-vos (dev):
external/coqutil/src/coqutil/Z/PushPullMod.v#L1
Coq.ZArith.ZArith has been replaced by Stdlib.ZArith.ZArith.
|
|
build-vos (dev):
external/coqutil/src/coqutil/Sorting/Permutation.v#L1
Coq.Sorting.Permutation has been replaced by Stdlib.Sorting.Permutation.
|
|
build-vos (dev):
external/stdpp/stdpp/base.v#L11
"From Coq" has been replaced by "From Stdlib".
|
|
build-vos (dev):
external/stdpp/stdpp/base.v#L12
"From Coq" has been replaced by "From Stdlib".
|
|
build-vos (dev):
external/stdpp/stdpp/base.v#L14
Coq.Program has been replaced by Stdlib.Program.
|
|
build (dev):
external/coqutil/src/coqutil/Z/Lia.v#L1
Coq.ZArith.ZArith has been replaced by Stdlib.ZArith.ZArith.
|
|
build (dev):
external/coqutil/src/coqutil/Z/div_mod_to_equations.v#L1
Coq.ZArith.BinInt has been replaced by Stdlib.ZArith.BinInt.
|
|
build (dev):
external/coqutil/src/coqutil/Word/Interface.v#L3
Coq.ZArith.BinIntDef has been replaced by Stdlib.ZArith.BinIntDef.
|
|
build (dev):
external/coqutil/src/coqutil/Word/Interface.v#L3
Coq.ZArith.BinInt has been replaced by Stdlib.ZArith.BinInt.
|
|
build (dev):
external/coqutil/src/coqutil/Z/Lia.v#L2
Coq.micromega.Lia has been replaced by Stdlib.micromega.Lia.
|
|
build (dev):
external/coqutil/src/coqutil/Z/PushPullMod.v#L1
Coq.ZArith.ZArith has been replaced by Stdlib.ZArith.ZArith.
|
|
build (dev):
external/coqutil/src/coqutil/Sorting/Permutation.v#L1
Coq.Sorting.Permutation has been replaced by Stdlib.Sorting.Permutation.
|
|
build (dev):
external/stdpp/stdpp/base.v#L11
"From Coq" has been replaced by "From Stdlib".
|
|
build (dev):
external/stdpp/stdpp/base.v#L12
"From Coq" has been replaced by "From Stdlib".
|
|
build (dev):
external/stdpp/stdpp/base.v#L14
Coq.Program has been replaced by Stdlib.Program.
|
|
build (8.19):
src/base_logic/lib/frac_coPset.v#L8
Ignored instance declaration for “fc_carrier”: “frac_coPset → discrete_fun (λ _ : positive, optionO fracR)” is not a class
|