aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-06-08Merge PR #12480: Don't suggest Proof using when no section variablesEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-06-08Merge PR #12471: Fix uncaught NotArity in inductive typePierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: ppedrot
2020-06-08Merge PR #12477: [sphinx] Fix regexp used in ↵Théo Zimmermann
coqdomain.CoqtopBlocksTransform.split_lines Reviewed-by: Zimmi48
2020-06-08Merge PR #12451: Fix Flocq build on Windows.Emilio Jesus Gallego Arias
2020-06-08Don't suggest Proof using when no section variablesGaëtan Gilbert
Fix #12447
2020-06-07[sphinx] Fix regexp used in coqdomain.CoqtopBlocksTransform.split_linesClément Pit-Claudel
2020-06-07Merge PR #12473: Match only a single line as the coqtop prompt in coqtop:: ↵Clément Pit-Claudel
directive
2020-06-06Match only a single line as the coqtop promptJim Fehrle
(the previous expression was including some expected output)
2020-06-06Merge PR #12380: Fix #12361 (indexing issues in the PDF)Théo Zimmermann
Ack-by: Zimmi48 Reviewed-by: jfehrle
2020-06-06Fix uncaught NotArity in inductive typeGaëtan Gilbert
Fixes #12390
2020-06-05Fix Flocq build in Windows add-ons.Théo Zimmermann
1. Fix casing of build_prep_overlay argument. Follow-up of 6cc6b87f997d7a5e848203b49bfedfaa96c53bb2 2. Call autoconf directly. Adapted from a9996619e2d2352e0e60faf4dbde78fa1549b2af
2020-06-05Merge PR #12336: Factorize code in hint declaration.Hugo Herbelin
Reviewed-by: herbelin
2020-06-05Merge PR #12450: Document known issue of Proof <term> with PG.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: erikmd Reviewed-by: jfehrle
2020-06-05Merge PR #12460: Add remaining 8.12+beta1 changelog entries.Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2020-06-05Merge PR #12459: Document incompatibility with Sphinx 3.Emilio Jesus Gallego Arias
Reviewed-by: cpitclaudel
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-05Add remaining 8.12+beta1 changelog entries.Théo Zimmermann
2020-06-05Document incompatibility with Sphinx 3.Théo Zimmermann
Cf. #12332
2020-06-05Fix version switcher when building with Dune.Théo Zimmermann
Closes #12395.
2020-06-05Fix comment.Théo Zimmermann
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> Remove note about Sphinx tradition.
2020-06-05[sphinx] Fix #12361Clément Pit-Claudel
2020-06-05[sphinx] Improve the error message printed for duplicate namesClément Pit-Claudel
2020-06-05[sphinx] Get rid of anonymous targets (Sphinx 2.3.1 doesn't like them)Clément Pit-Claudel
https://github.com/sphinx-doc/sphinx/issues/7701
2020-06-05[sphinx] Remove most pylint warningsClément Pit-Claudel
2020-06-05Merge PR #11707: Split the Reductionops machine from the cbn oneMaxime Dénès
Reviewed-by: maximedenes
2020-06-04Tweak wording.Théo Zimmermann
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-06-04Document known issue of Proof <term> with PG.Théo Zimmermann
See #12444.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-12 08:24:27 +0000