aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2019-04-02Merge PR #8984: Declare initial hint databases in preludePierre-Marie Pédrot
Ack-by: JasonGross Reviewed-by: ppedrot
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-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.
2019-03-26Overlays for HoTT, Ltac2, and UniMathVincent Laporte
2019-03-22Merge PR #9602: [kernel] termination checking: backtrack on stuck case, fix, ↵Maxime Dénès
proj Ack-by: gares Reviewed-by: mattam82 Reviewed-by: maximedenes
2019-03-21Merge PR #9774: Remove clutter by moving historic unmaintained dev/doc files ↵Emilio Jesus Gallego Arias
to an archive subfolder. Reviewed-by: ejgallego
2019-03-20Add overlays for printer API changesMaxime Dénès
2019-03-20Stop accessing proof env via Pfedit in printersMaxime Dénès
This should make https://github.com/coq/coq/pull/9129 easier.
2019-03-19Merge PR #9647: [default.nix] Enable parallel buildThéo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: ejgallego
2019-03-19Fixed incompatibility between new cygwin pkg-config and duneMichael Soegtrop
2019-03-19[win] Mostly fixed GTK3 CoqIDE Windows build (icons don't work, only 64 but ↵Michael Soegtrop
tested, only binary GTK)
2019-03-19[coqide] [ci] Update GTK toolchain to lablgtk3Emilio Jesus Gallego Arias
- Update Docker images to install compatible version of lablgtk3 - We remove unnecesary variables from configure. - We fix path detection of GTK libs in makefile
2019-03-19CoqIDE: Adapt configuration to require lablgtk3 and gtksourceview3.Hugo Herbelin
2019-03-18[nix] Update reference to nixpkgsVincent Laporte
2019-03-18[nix] Move nixpkgs.nix into the dev/ directoryVincent Laporte
2019-03-18[nix-ci] Use “master” versions of “coq-ext-lib” and “simple-io”Vincent Laporte
2019-03-18[nix-ci] Share the reference to nixpkgs with default.nixVincent Laporte
2019-03-17iconv bedrock2 CI output to UTF-8Andres Erbsen
The timing diff script dies badly on non-utf8 input (https://github.com/coq/coq/issues/9767).
2019-03-16Add test-suite to Paramcoq CIPierre Roux
2019-03-15Remove clutter by moving historic unmaintained dev/doc files to an archive ↵Théo Zimmermann
subfolder.
2019-03-14Overlays for SPropGaëtan Gilbert
2019-03-14Documentation for SPropGaëtan Gilbert
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
Kernel should be mostly correct, higher levels do random stuff at times.
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
Note currently it's impossible to define inductives in SProp because indtypes.ml and the pretyper aren't fully plugged.
2019-03-13Merge PR #9748: [dune] Add shim for coqtop.byteThéo Zimmermann
Reviewed-by: Zimmi48 Reviewed-by: gares
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 07:15:32 +0000