aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-09-22Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.Hugo Herbelin
2020-09-22Merge PR #13046: Small optimization of acyclic graph merge operationcoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-09-22Merge PR #13050: [ci/gitlab/cachix] Avoid running in trouble when calling ↵coqbot-app[bot]
git fetch --unshallow Reviewed-by: SkySkimmer
2020-09-22Merge PR #13049: [configure] Fix version checks for lablgtk and zarithcoqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: vbgl Ack-by: Zimmi48 Ack-by: JasonGross
2020-09-22Merge PR #13063: Make print-pretty-timed robust against non-output-sync logscoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-09-21Merge PR #13057: Adding debugging printers for Intmapcoqbot-app[bot]
Reviewed-by: ppedrot
2020-09-21Make print-pretty-timed robust against non-output-sync logsJason Gross
Also pass `--output-sync` on the CI, as suggested in https://github.com/coq/coq/pull/12653#issuecomment-696226093, to protect against this failure mode. Fixes #13062
2020-09-21Bump nixpkgs to get zarith 1.10.Théo Zimmermann
2020-09-21Merge PR #12723: dune: pass -bin-annot to configurecoqbot-app[bot]
Reviewed-by: ejgallego
2020-09-19Merge PR #13052: Clean up Dnet implementationHugo Herbelin
Reviewed-by: herbelin
2020-09-18Merge PR #13055: Fix Removed in Sphinx 4 deprecations.coqbot-app[bot]
Reviewed-by: jfehrle
2020-09-18Merge PR #12963: Formally deprecate the double induction tactic.Hugo Herbelin
Reviewed-by: VincentSe Ack-by: herbelin Ack-by: olaure01
2020-09-18Adding debugging printers for Intmap.Hugo Herbelin
2020-09-18Merge PR #13051: Improve `simple apply` examplecoqbot-app[bot]
Reviewed-by: Zimmi48
2020-09-18Merge PR #13043: [ci] call dmesg after quick/async jobs to detect OOMcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-09-18Fix Removed in Sphinx 4 deprecations.Théo Zimmermann
2020-09-18Make `simple apply in ...` point to `simple apply`Maxime Dénès
Instead, the example was duplicated.
2020-09-18[ci] [dmesg] save as artifactEnrico Tassi
2020-09-18Improve `simple apply` exampleMaxime Dénès
The example showing the difference between `apply` and `simple apply` used to depend on the order and the heuristics used on unification problems. We make it independent for better clarity and stability. Fixes https://github.com/coq/coq/issues/13023
2020-09-18Merge PR #12610: [leminv] [declare] Use higher-level Declare API.Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-09-18Remove unused API from Dn.Pierre-Marie Pédrot
2020-09-18Clean up a bit the implemenation of dnets.Pierre-Marie Pédrot
We use higher-level combinators instead of composition of low-level ones.
2020-09-18Remove dead code in dnets.Pierre-Marie Pédrot
The boolean assumedly used to cut recursion was always set to true, since its introduction in 64ac193.
2020-09-18Merge PR #13027: [vernac] Don't allow attributes on print / checkcoqbot-app[bot]
Reviewed-by: Zimmi48
2020-09-17[ci/gitlab/cachix] Avoid running in trouble when calling git fetch --unshallow.Théo Zimmermann
2020-09-17Merge PR #13007: [build] Don't link `num` anymore in Coqcoqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: vbgl Ack-by: Zimmi48 Ack-by: vbgl
2020-09-17[configure] Fix version checks for lablgtk and zarithEmilio Jesus Gallego Arias
Fixes #13041 #13047 Configure is quite messy, but we will improve it once we can link it with findlib and move to dune [that will actually allow to remove all ad-hoc calls to `ocamlfind` in favor of `findlib` code.
2020-09-17Be more efficient when generating the merge of ltle maps in AcyclicGraph.Pierre-Marie Pédrot
We try to avoid reallocating the map in two different ways. - We only add a value when actually needed. - We compute the union of maps with the first element as a starting point.
2020-09-17Do not allocate intermediate sets in universe refreshing.Pierre-Marie Pédrot
A set was created only to be folded over. Since the list is ensured to be duplicate-free, there is no point in creating the former, we just fold over the list directly.
2020-09-17[leminv] Use higher-level Declare API.Emilio Jesus Gallego Arias
2020-09-17[leminv] Remove unused catch.Emilio Jesus Gallego Arias
2020-09-17[install] Rewording of primitive floats.Emilio Jesus Gallego Arias
As suggested in the PR review. Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-09-17[build] Don't link `num` anymore in CoqEmilio Jesus Gallego Arias
After #8743 we don't depend on `num` anymore in the codebase; thus we drop the dependency. This could create problems for plugins relying on this implicit linking.
2020-09-17Merge PR #13024: [CI] Always upload artifactscoqbot-app[bot]
Reviewed-by: Zimmi48
2020-09-17[ci] call dmesg after quick/async jobs to detect OOMEnrico Tassi
2020-09-17Formally deprecate the double induction tactic.Pierre-Marie Pédrot
The doc states it is deprecated since 1386cd9 but this was ages before the deprecation mechanism existed.
2020-09-16Merge PR #13008: Use fresher names in eqschemesHugo Herbelin
Reviewed-by: herbelin Reviewed-by: ppedrot
2020-09-16Merge PR #13015: Propagate zarith dependency.Vincent Laporte
Reviewed-by: vbgl
2020-09-16Merge PR #8743: [micromega] Switch from `Big_int` to ZArith.BESSON Frederic
Ack-by: JasonGross Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: fajb Ack-by: liyishuai Ack-by: maximedenes Ack-by: ppedrot Ack-by: soraros Ack-by: thery Ack-by: vbgl
2020-09-15[vernac] Don't allow attributes on print / checkEmilio Jesus Gallego Arias
Fixes #11661
2020-09-15[micromega] Use `minus_one` built-in zarith constant.Emilio Jesus Gallego Arias
2020-09-15[zarith] [micromega] Bump to 1.10 and remove some hacksEmilio Jesus Gallego Arias
In particular, behavior of `Z.gcd` and `Z.lcm` has been fixed in 1.10, see https://github.com/ocaml/Zarith/issues/58
2020-09-15Updated .csdp.cache.test-suite and minor fixesBESSON Frederic
- merlin.in : added zarith - test-suite/Makefile remove .csdp.cache on make clean updated .csdp.cache.test-suite
2020-09-15[micromega] [test-suite] Update csdp cache for num -> zarith migrationEmilio Jesus Gallego Arias
2020-09-15[micromega] Migrate from num to zarithEmilio Jesus Gallego Arias
We still link num in `coqc` , that will be removed in a separate step. Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
2020-09-15[micromega] call csdpcert using path.Emilio Jesus Gallego Arias
2020-09-15Merge PR #13016: Remove deprecated Extraction Language command value "Ocaml"Pierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: pi8027 Reviewed-by: ppedrot
2020-09-15Merge PR #12972: [ci] [docker] Up testing to OCaml 4.11.1coqbot-app[bot]
Reviewed-by: Zimmi48
2020-09-14[CI] Always upload artifactsJason Gross
In order to support the workflow where coqbot automatically turns failing CI jobs into minimized examples for the test-suite easily (https://github.com/coq/bot/issues/107), we want to be able to get all of the .v files and all of the generated .vo and .glob files in the artifact, even when the build fails.
2020-09-14Remove deprecated Extraction Language command value "Ocaml"Jim Fehrle
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 09:02:11 +0000