aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-06-05Merge PR #12437: Fix ONLY_WINDOWS in .gitlab-ci.yml.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-06-05Merge PR #12397: Fix #12280: do not use xindy to avoid build failures on ↵Emilio Jesus Gallego Arias
some machines. Reviewed-by: SkySkimmer Reviewed-by: cpitclaudel
2020-06-05Merge PR #12456: Fix version switcher when building with Dune.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-06-05Adjust list of versions in version switcher.Théo Zimmermann
- Use the name 'dev' instead of 'master' because it is less cryptic. - Add the 'v8.12' branch. - Use the branch version only for active branches, and the latest patch-level release for the rest.
2020-06-05Fix version switcher when building with Dune.Théo Zimmermann
Closes #12395.
2020-06-05Merge PR #11707: Split the Reductionops machine from the cbn oneMaxime Dénès
Reviewed-by: maximedenes
2020-06-04Merge PR #12440: [declare] Hide internals of variable declaration entries.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-06-04Move the Cbn module to tactics/.Pierre-Marie Pédrot
2020-06-04Further cleanup.Pierre-Marie Pédrot
We factorize code between Cbn and Reductionops, and remove dead code as well.
2020-06-04Move the cbn reduction to its own file, and simplify the RAKAM accordingly.Pierre-Marie Pédrot
2020-06-03Merge PR #12419: Various cleanups in eautoHugo Herbelin
Reviewed-by: herbelin
2020-06-03[declare] Hide internals of variable declaration entries.Emilio Jesus Gallego Arias
In particular this avoids exposing `Evd.side_effects proof_entry` in the API.
2020-06-03Merge PR #12427: Add a dependency of coq_makefile's coqdep target into ↵Enrico Tassi
_CoqProject Reviewed-by: JasonGross
2020-06-03Merge PR #12337: Move CoqIDE to its own folderEnrico Tassi
Reviewed-by: MSoegtropIMC Reviewed-by: Zimmi48 Reviewed-by: gares Reviewed-by: ppedrot
2020-06-03Fix ONLY_WINDOWS in .gitlab-ci.yml.Théo Zimmermann
2020-06-02Move CoqIDE to its own folderMaxime Dénès
The will make it possible to put a VsCoq toplevel in `ide/vscoq`.
2020-06-02Merge PR #12412: Reduce options passed to workersEnrico Tassi
Ack-by: SkySkimmer Reviewed-by: gares
2020-06-02Merge PR #11974: Require in Section: warning is now about fragility not ↵Emilio Jesus Gallego Arias
deprecation. Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2020-06-02Enforce statically the invariant that a goal comes with its database in eauto.Pierre-Marie Pédrot
2020-06-02Simplify Eauto.e_trivial_resolve.Pierre-Marie Pédrot
No need to create various mapping of lists when a filter would suffice.
2020-06-02Factor the computation of head constant in Eauto resolution.Pierre-Marie Pédrot
2020-06-02Make explicit the computation of lists of goals in eauto.Pierre-Marie Pédrot
2020-06-02Some wrapper cleanup around eauto.Pierre-Marie Pédrot
2020-06-01Merge PR #12396: Release notes 8.12Emilio Jesus Gallego Arias
Reviewed-by: ejgallego Ack-by: jfehrle
2020-06-01Merge PR #12422: Fixes #12418: an assert false in inference of return clauseEmilio Jesus Gallego Arias
Reviewed-by: gares
2020-06-01Merge PR #12431: [ci] Split fiat-crypto into non-OCaml and OCamlGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-31[ci] Split fiat-crypto into non-OCaml and OCamlJason Gross
Note that this should reduce the overall build time of fiat-crypto related targets by about 10--20 minutes, as I've removed the heaviest jobs (about 25--30 minutes in serial) from the OCaml target. I'd like to keep the OCaml target around just to make sure that Coq doesn't introduce a change to extraction that breaks compilation of extracted OCaml code. See https://github.com/ocaml/ocaml/issues/7826 for the issue tracking performance of compiling the extracted OCaml code (and perhaps there should be another issue opened on the OCaml bug tracker about flambda on the fiat-crypto extracted files?) Alternative to #12405 Closes #12405 Fixes #12400
2020-05-30Coq_makefile: adding a dependency of .coqdeps on _CoqProject.Hugo Herbelin
2020-05-29Merge PR #12393: [declare] Miscellaneous nits from my main dev treeGaëtan Gilbert
Reviewed-by: SkySkimmer
2020-05-29Require in Section: warning is now about fragility not deprecation.Gaëtan Gilbert
2020-05-29Change log for #12422.Hugo Herbelin
2020-05-29Fixes #12418 (inference of return clause meets assert false).Hugo Herbelin
This is a quick fix to avoid the anomaly, with a fallback on before b1b8243b7fc.
2020-05-29Merge PR #12421: Fixes for compilation without native dynlinkEmilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: ppedrot
2020-05-28Merge PR #12399: Remove the prolog tactic.Théo Zimmermann
Reviewed-by: Zimmi48
2020-05-28Adding missing DECLARE PLUGIN so that compilation with -natdynlink no works.Hugo Herbelin
2020-05-28Fixing compilation with -natdynlink no.Hugo Herbelin
This complements #11407 about storing digests of modules.
2020-05-27Merge PR #12389: Small coq_makefile improvement.Enrico Tassi
Reviewed-by: gares
2020-05-27Adding changelog.Martin Bodin
2020-05-27Promoting COQLIBINSTALL and COQDOCINSTALL in coq_makefile to the parameters ↵Martin Bodin
section.
2020-05-27Add more changelog entries which have been backported to v8.12.Théo Zimmermann
2020-05-27[changelog/8.12] Wording improvements.Théo Zimmermann
2020-05-27[changelog/8.12] Use sections and provide a local TOC.Théo Zimmermann
2020-05-27[changelog/8.12] Split misc entries out in more relevant sections.Théo Zimmermann
2020-05-27Changelog entries for the 8.12 changes to the reference manual.Théo Zimmermann
2020-05-27Release notes for 8.12.Théo Zimmermann
2020-05-27Fix changelog for #11986.Théo Zimmermann
2020-05-27Merge PR #12408: Fix output tests for location errors when running in async ↵Emilio Jesus Gallego Arias
mode. Reviewed-by: JasonGross Reviewed-by: ejgallego
2020-05-26[declare] Split univs_poly_private in close_proofEmilio Jesus Gallego Arias
A step towards enforcing some more static invariants.
2020-05-26[declare] Factor common universe computation in close proof.Emilio Jesus Gallego Arias
2020-05-26[declare] Split univs_deferred in close_proofEmilio Jesus Gallego Arias
A step towards enforcing some more static invariants.
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 14:23:01 +0000