aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2020-10-12Lowercase variables in git_downloadGaëtan Gilbert
2020-10-12elpi 1.11.4Enrico Tassi
2020-10-10Prim.pattern_ident takes a location and its synonymous pattern_identref is ↵Hugo Herbelin
deprecated.
2020-10-10Merge PR #13164: [bench] Dump the vo size difference.coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-10-09Merge PR #13088: [stm] move par: to comTacticcoqbot-app[bot]
Reviewed-by: SkySkimmer Reviewed-by: ppedrot Reviewed-by: ejgallego
2020-10-09overlay for mtac2Enrico Tassi
2020-10-09[bench] Dump the vo size difference.Pierre-Marie Pédrot
2020-10-09overlay for minim-prop-tosetGaëtan Gilbert
2020-10-08Add overlays for Coq-Equations, aac-tactics.Hugo Herbelin
2020-10-08Dropping the misleading int argument of Pp.h.Hugo Herbelin
An h-box inhibits the breaking semantics of any cut/spc/brk in the enclosed box. We tentatively replace its occurrence by an h or hv, assuming in particular that if the indentation is not 0, an hv box was intended.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 21:15:14 +0000