Commit eacc204
committed
[vendor] [deps] Bump Rocq (and Rocq-stdlib deps)
For overlays rocq-prover/rocq#20962 and rocq-prover/rocq#20917
We still keep our stdlib overlay due to
rocq-prover/stdlib#2011 parent 9d94cae commit eacc204
3 files changed
+3
-3
lines changedSubmodule coq updated from d2ee654 to 4015c7e
Submodule coq-stdlib updated from fb92a5f to e307464
Submodule coq-waterproof updated 72 files
- .devcontainer/Dockerfile+2-2
- .github/workflows/build-with-make.yml-28
- .github/workflows/build.yml+1-1
- .github/workflows/doc.yml+1-1
- CHANGES.md+2-2
- _CoqProject+6-1
- _CoqProjectForMake+5-1
- src/exceptions.ml+21
- src/exceptions.mli+6-1
- src/g_waterproof.mlg+29
- src/hint_dataset_declarations.ml+1-1
- src/proofutils.ml+6-6
- src/waterproof.mlpack+1
- src/wp_auto.ml-1
- src/wp_bullets.ml+191
- src/wp_bullets.mli+32
- src/wp_eauto.ml-1
- tests/Notations/Sets.v+12
- tests/libs/Sets.v+47
- tests/tactics/Assume.v+36-27
- tests/tactics/Because.v+5-5
- tests/tactics/BothStatements.v+5-5
- tests/tactics/Choose.v+8
- tests/tactics/Claims.v+2-2
- tests/tactics/Conclusion.v+4-5
- tests/tactics/Define.v+6
- tests/tactics/Either.v+46-46
- tests/tactics/Help.v+7-6
- tests/tactics/Induction.v+9-9
- tests/tactics/ItHolds.v+34-28
- tests/tactics/ItSuffices.v+9-9
- tests/tactics/Postpone.v+3-3
- tests/tactics/Specialize.v+16-8
- tests/tactics/Take.v+18-1
- tests/tactics/TakeSuchThat.v+4-4
- tests/tactics/ToShow.v+8-8
- tests/tactics/Unfold.v+3-3
- tests/util/Bullets.v+83
- theories/Automation/Hints.v+5
- theories/Libs/Analysis/ContinuityDomainNat.v+54-54
- theories/Libs/Analysis/ContinuityDomainR.v+32-32
- theories/Libs/Analysis/LimsupLiminfBolzano.v+118-118
- theories/Libs/Analysis/MetricSpaces.v+19-19
- theories/Libs/Analysis/OpenAndClosed.v+11-11
- theories/Libs/Analysis/Sequences.v+175-176
- theories/Libs/Analysis/SequentialAccumulationPoints.v+20-20
- theories/Libs/Analysis/Series.v+39-38
- theories/Libs/Analysis/StrongInductionIndexSequence.v+14-15
- theories/Libs/Analysis/Subsequences.v+39-39
- theories/Libs/Analysis/SubsequencesMetric.v+39-39
- theories/Libs/Analysis/SupAndInf.v+288-289
- theories/Libs/Reals.v+4-4
- theories/Libs/Sets.v+28
- theories/Notations/Sets.v+37-18
- theories/Tactics/Assume.v+25-2
- theories/Tactics/Because.v+2-2
- theories/Tactics/BothStatements.v+2-2
- theories/Tactics/Choose.v+1-1
- theories/Tactics/Claims.v+1-1
- theories/Tactics/Conclusion.v+8-7
- theories/Tactics/Define.v+1-1
- theories/Tactics/Either.v+2-2
- theories/Tactics/Induction.v+1-1
- theories/Tactics/ItHolds.v+27-26
- theories/Tactics/ItSuffices.v+5-5
- theories/Tactics/Specialize.v+2-2
- theories/Tactics/Take.v+3-2
- theories/Tactics/ToShow.v+4-4
- theories/Tactics/Unfold.v+2-2
- theories/Util/BySince.v+20-14
- theories/Util/Goals.v+1-1
- theories/Util/TypeCorrector.v+1-1
0 commit comments