aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2019-05-05New infrastructure for the unreleased changelog.Théo Zimmermann
Move existing entries.
2019-04-29Merge PR #9987: Fix #9180 by reverting #9249 and #8187Emilio Jesus Gallego Arias
Reviewed-by: maximedenes
2019-04-29Merge PR #9935: [api] [proof] Alert users that `Vernacstate.Proof_global` is ↵Maxime Dénès
not to be used. Ack-by: ejgallego Ack-by: gares Reviewed-by: maximedenes
2019-04-29Merge PR #9925: [vm] Protect accu and coq_envMaxime Dénès
Ack-by: Zimmi48 Reviewed-by: maximedenes Ack-by: proux01 Reviewed-by: vbgl
2019-04-29Revert #8187Vincent Laporte
2019-04-24[coq_makefile] Enforce warn_error for plugins.Emilio Jesus Gallego Arias
The amount of dangerous warnings in plugins is out of hand, including some very serious ones. As Coq developers are maintaining plugins these days it makes sense to require the contributions to follow the same coding discipline as in the main tree, thus we require the set of warnings fatal warnings to be the same in Coq and in plugins. We don't mark deprecation as fatal as to allow time for migration. Fixes #6974
2019-04-20overlay for elpiEnrico Tassi
2019-04-20update elpi to version 1.2Enrico Tassi
2019-04-17Merge PR #9891: [CI] Build CoqIDE for macOS on AzurePierre-Marie Pédrot
Reviewed-by: SkySkimmer Reviewed-by: ejgallego Ack-by: ppedrot Ack-by: vbgl
2019-04-16[doc] Changes for coq/coq#9165Emilio Jesus Gallego Arias
2019-04-16[ci] Overlays for coq/coq#9165Emilio Jesus Gallego Arias
2019-04-16[CI/Azure/macOS] Install Coq into an artifactVincent Laporte
2019-04-15Update critical-bugsPierre Roux
2019-04-10Overlays for Global removal in pretyperMaxime Dénès
2019-04-09[api] [proof] Alert users that `Vernacstate.Proof_global` is not to be used.Emilio Jesus Gallego Arias
We alert users that `Vernacstate.Proof_global` is a Coq internal module and should not be used to workaround lack of state threading.
2019-04-05[native compiler] Fix critical bug with primitive projectionsMaxime Dénès
Since e1e7888, stuck projections were not computed correctly. Fixes #9684
2019-04-05Merge PR #8764: Add parsing of decimal constants (e.g., 1.02e+01)Emilio Jesus Gallego Arias
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Ack-by: gares Ack-by: herbelin Ack-by: ppedrot Ack-by: proux01
2019-04-04[CI] Fix build of math-comp dependenciesMaxime Dénès
We were incorrectly calling the global `install` target even when building only subcomponents of the library.
2019-04-04[dune] Fix include object dirs.Emilio Jesus Gallego Arias
In Dune >= 1.8 object dirs have changed; this should be stable for a while, however we want a more robust setup for sure, which I think it should be able to be implemented when we have a single build system.
2019-04-02Merge PR #9668: Consolidate credits and changelog information in a single place.Clément Pit-Claudel
Reviewed-by: cpitclaudel Reviewed-by: vbgl
2019-04-02Merge PR #8984: Declare initial hint databases in preludePierre-Marie Pédrot
Ack-by: JasonGross Reviewed-by: ppedrot
2019-04-02Add overlaysPierre Roux
2019-04-01[CI] Disable Coquelicot on WindowsVincent Laporte
2019-04-01[CI] Coquelicot: use “master” development versionVincent Laporte
2019-04-01Merge PR #9870: Minor refactoring in canonical structuresEnrico Tassi
Reviewed-by: Zimmi48 Reviewed-by: gares Reviewed-by: ppedrot
2019-04-01Merge PR #9815: Multiple payload types in tokensPierre-Marie Pédrot
Reviewed-by: ppedrot Ack-by: proux01
2019-04-01Merge PR #9871: CI: add mit-pdos/argosyEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-04-01Merge PR #9872: Fix timing diff script to support non-utf8Emilio Jesus Gallego Arias
Reviewed-by: ejgallego Reviewed-by: jashug
2019-03-31Add overlayPierre Roux
2019-03-31Merge PR #9733: [lexer] keyword protected quotation token for arbitrary textPierre-Marie Pédrot
Ack-by: Zimmi48 Ack-by: ejgallego Ack-by: gares Reviewed-by: ppedrot
2019-03-31Revert "iconv bedrock2 CI output to UTF-8"Jason Gross
This reverts commit 1eb8b9dc3ff0e464c9cd6c7f12a1c9db4fa57423. This commit is no longer necessary
2019-03-31CI: add mit-pdos/argosyTej Chajed
2019-03-31overlay for ltac2Enrico Tassi
2019-03-31[dune] typoEnrico Tassi
2019-03-31Move content of COMPATIBILITY to Changes chapter.Théo Zimmermann
2019-03-30Error when [foo.(bar)] is used with nonprojection [bar]Gaëtan Gilbert
(warn if bar is a nonprimitive projection)
2019-03-30Overlay for ElpiVincent Laporte
2019-03-29Merge PR #9858: Fix top_printers after removal of imperative stateEmilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-03-29Merge PR #9860: [dune] Fix shim quoting and add coqc wrapper.Théo Zimmermann
Reviewed-by: Zimmi48
2019-03-28[dune] Fix shim quoting and add coqc wrapper.Emilio Jesus Gallego Arias
The quoting was incorrect thus scripts didn't properly work.
2019-03-28Fix top_printers after removal of imperative stateGaëtan Gilbert
There's never a proof available in ocamldebug I don't know about Drop.
2019-03-28Use only lowercase for unimath in CI scriptsGaëtan Gilbert
Fix #9845
2019-03-27[proof_global] [ci] Overlays for removal of imperative state.Emilio Jesus Gallego Arias
2019-03-27[vernac] Adapt to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-27Merge PR #9807: Fix CoqIDE progress bar.Enrico Tassi
Reviewed-by: Zimmi48
2019-03-27[nix] Update reference to nixpkgsVincent Laporte
2019-03-27Merge PR #9837: Fix some critical-bugs informationsThéo Zimmermann
Reviewed-by: Zimmi48
2019-03-26Fix reproduction info for some past critical bugsGaëtan Gilbert
- test-suite/bugs/closed/xx.v renamed to .../bug_xx.v - test-suite/failure/inductive4.v is now .../inductive.v - repro for #4157 now added to the repo (it was in an unmerged commit on @herbelin's repo) - commit message of 244d7a9aa contains a repro for its bug (I didn't bother adding to the test suite as a return of the bug could just as well use different strings so the specific repro wouldn't test anything useful)
2019-03-26Incorrect details in critical bug info (prop_set_proof_irrelevance)Gaëtan Gilbert
2019-03-26Improve the backport script.Guillaume Melquiond
It now uses the origin/master branch rather than the master branch, thus avoiding the need for local merges. More importantly, it no longer creates a subshell in case of conflicts, but instead gives control back to the user. Once conflicts are solved, it suffices to relaunch the script (instead of exiting the subshell). The reason is that, otherwise, there was no sane way of giving up a backport, due to the infinite subshell loop.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 20:22:09 +0000