aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2020-10-08update for Iris build system changesRalf Jung
2020-10-06Define a new type instance_flag instead of using [unit option]Gaëtan Gilbert
2020-10-04Merge PR #13096: Drop prefixes from non-terminal names, e.g. "constr:constr" ↵coqbot-app[bot]
-> "constr" Reviewed-by: herbelin Ack-by: Zimmi48
2020-10-04Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."Jim Fehrle
2020-10-03Merge PR #12985: Remove ocamlformat from the linter and the pre-commit hook.coqbot-app[bot]
Reviewed-by: Zimmi48 Reviewed-by: gares Reviewed-by: maximedenes Reviewed-by: Matafou Ack-by: ejgallego
2020-10-02{new,setoid_}ring -> ringMaxime Dénès
I believe this renaming makes it easier for new contributors to discover the code of `ring`.
2020-09-28Document the ocamlformat changes.Pierre-Marie Pédrot
2020-09-28Remove the linter ocamlformat pass.Pierre-Marie Pédrot
2020-09-28Remove the ocamlformat git hook.Pierre-Marie Pédrot
2020-09-28CI script wrapper now requires PythonMaxime Dénès
2020-09-23Fix issue #13065 - Windows CI brokenMichael Soegtrop
2020-09-23Merge PR #12977: Statically ensure that only polymophic hint terms come with ↵coqbot-app[bot]
a context. Reviewed-by: mattam82
2020-09-22Add overlay for Equations.Hugo Herbelin
2020-09-22Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.Hugo Herbelin
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-18Adding debugging printers for Intmap.Hugo Herbelin
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-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-14[nix] Update ref for ocamlformat 0.15Emilio Jesus Gallego Arias
Co-authored-by: Théo Zimmermann <theo.zimmi@gmail.com>
2020-09-14[ci] [docker] Up testing to OCaml 4.11.1Emilio Jesus Gallego Arias
- `odoc` must be bumped to support 4.11
2020-09-13Add overlays.Pierre-Marie Pédrot
2020-09-11[ci] [mathcomp] run the test suiteEnrico Tassi
2020-09-10Add simple-io to dev/ci/nix.Théo Zimmermann
2020-09-04Merge PR #12969: CI: build Iris examples instead of lambda-Rustcoqbot-app[bot]
Reviewed-by: SkySkimmer
2020-09-03[bench] Only upload some filesJason Gross
We will now also record a listing of all files that we could have uploaded, in case we want to know what's available to upload in the future.
2020-09-03[bench] Also upload the raw timing files, etcJason Gross
2020-09-03Merge PR #12968: Replace `frozen` by `allowed` evars in evarconv, and delay themPierre-Marie Pédrot
Reviewed-by: ppedrot
2020-09-03Merge PR #12899: [bench] Update bench script with better urls and more infoPierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: ppedrot
2020-09-03Add Equations overlayMaxime Dénès
2020-09-02fix grepping for the Iris commitRalf Jung
2020-09-02CI: build Iris examples instead of lambda-RustRalf Jung
2020-09-01Merge PR #12892: Update update_global_env usagePierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: gares Reviewed-by: ppedrot
2020-08-31Add zarith to the include path for ocamldebug-coqJasper Hugunin
2020-08-31Merge PR #12958: Fix load_printers after zarithcoqbot-app[bot]
Reviewed-by: ejgallego
2020-08-31Update update_global_env usageGaëtan Gilbert
- take just a ugraph instead of the whole env - rename to update_sigma_univs - push global env lookup a bit further up - fix vernacinterp call to update all surrounding proofs, not just the top one - flip argument order for nicer partial applications
2020-08-31Merge PR #12875: Further extensions of About wrt Arguments and renamingcoqbot-app[bot]
Reviewed-by: SkySkimmer Ack-by: herbelin
2020-08-31Fix load_printers after zarithGaëtan Gilbert
2020-08-28Adding overlay for coq-elpi.Hugo Herbelin
2020-08-27[numeral] [plugins] Switch from `Big_int` to ZArith.Emilio Jesus Gallego Arias
We replace Coq's use of `Big_int` and `num` by the ZArith OCaml library which is a more modern version. We switch the core files and easy plugins only for now, more complex numerical plugins will be done in their own commit. We thus keep the num library linked for now until all plugins are ported. Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
2020-08-27Merge PR #12849: Rename VM-related kernel/cfoo files to kernel/vmfooPierre-Marie Pédrot
Reviewed-by: gares Reviewed-by: ppedrot Reviewed-by: silene
2020-08-26Use the lite variants of performance tests in the bench default packages.Pierre-Marie Pédrot
They are much faster and should be as informative as their heavy counterparts. I have been forgetting to do that for a long time already.
2020-08-26Merge PR #12904: Move bench job definition to its own filePierre-Marie Pédrot
Reviewed-by: ppedrot
2020-08-25Move bench job definition to its own fileGaëtan Gilbert
This focuses review requests to bench-maintainers instead of sharing with ci-maintainers
2020-08-25Remove useless commit guessing logicJason Gross
On GitLab, we don't need to base the job info on the PR number, since it ought to be available from the git repo. Removing the logic will make the bench infrastructure more uniform.
2020-08-25[bench] Update bench script with better urls and more infoJason Gross
2020-08-25Merge PR #12801: Put cyclic numbers in sort Set instead of TypeAnton Trunov
Ack-by: Zimmi48 Reviewed-by: anton-trunov
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 22:06:15 +0000