aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2019-12-06Adding overlay for Quickchick PR#145.Hugo Herbelin
2019-12-06Moving the diversity of constr printers to a label style.Hugo Herbelin
This allows to give access to all printing options (e.g. a scope or being-in-context) to every printer w/o increasing the numbers of functions.
2019-12-06Merge PR #11174: [dune] Update to dune language version 2.0Théo Zimmermann
Reviewed-by: Zimmi48
2019-12-04Overlay for ELPIHugo Herbelin
2019-12-04[dune] Update to dune language version 2.0Emilio Jesus Gallego Arias
This is the minimal set of changes requires for Coq to build under 2.0 mode. We may likely take advantage of some more new features. Note that Dune 2.0 requires OCaml >= 4.06.0, OPAM allows to use Dune in older versions as it will install a secondary compiler.
2019-12-02Remove deprecated compat modifier of Notation / Infix commands.Théo Zimmermann
And simplify a lot the compatibility infrastructure following this. Update dev/tools/update-compat.py Remove much complexity. Co-authored-by: Jason Gross <jgross@mit.edu>
2019-12-02[ci] [sf] Add authentication to artifact download.Emilio Jesus Gallego Arias
It seems we need to pass the token to the actual artifact download.
2019-12-02[CI] Test latest artifacts of SF instead of the stable versionMaxime Dénès
2019-11-29Merge PR #10931: Add types of changes to changelog entries.Emilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: ejgallego
2019-11-28Update README and make-changelog tool following introduction of changelog types.Théo Zimmermann
2019-11-27[ci] Split out the dependencies of fiat-cryptoJason Gross
2019-11-27[ci] Build slightly more in the fiat-crypto targetJason Gross
This adds a couple extra files, but not many.
2019-11-27[release] Update files for 8.12 release per release process.Emilio Jesus Gallego Arias
2019-11-26Fix #11039: proof of False with template poly and nonlinear universesGaëtan Gilbert
Using the parameter universes in the constructor causes implicit equality constraints, so those universes may not be template polymorphic. A couple types in the stdlib were erroneously marked template, which is now detected. Removing the marking doesn't actually change behaviour though. Also fixes #10504.
2019-11-25Error fatally if update-compat.py gets no flagJason Gross
c.f. https://github.com/coq/coq/pull/11032#issue-335944369 Also, change the default from python2 to python3 for update-compat while we're at it, and update file unicode handling accordingly. (Note that this file still works with both python2 and python3.)
2019-11-21Merge PR #11154: add tlc to ci; please proof read very carefully and test. ↵Emilio Jesus Gallego Arias
thanks Reviewed-by: SkySkimmer Reviewed-by: ejgallego
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
We also remove trailing whitespace. Script used: ```bash for i in `find . -name '*.ml' -or -name '*.mli' -or -name '*.mlg'`; do expand -i "$i" | sponge "$i"; sed -e's/[[:space:]]*$//' -i.bak "$i"; done ```
2019-11-21add tlc to ci; please proof read very carefully and test. thankscharguer
2019-11-12Printing name of change log file in changelog script.Hugo Herbelin
2019-11-12Expand documentation about generating a Docker image.Pierre-Marie Pédrot
2019-11-08Merge PR #11042: The "univ poly can capture global univs" checker side bug ↵Théo Zimmermann
is fixed Reviewed-by: Zimmi48
2019-11-07The "univ poly can capture global univs" checker side bug is fixedGaëtan Gilbert
(by the checker refactor AFAICT) + fix commit for the coqtop side fix (it got rebased at some point) Close #10705
2019-11-05overlayEnrico Tassi
2019-11-05elpi 1.8Enrico Tassi
2019-11-01Merge PR #9867: Add primitive floats (binary64 floating-point numbers)Maxime Dénès
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: ejgallego Reviewed-by: maximedenes Ack-by: proux01 Ack-by: silene Ack-by: vbgl
2019-11-01Merge PR #11015: [Nix] Update reference to nixpkgsThéo Zimmermann
Reviewed-by: Zimmi48
2019-11-01Add overlaysPierre Roux
2019-11-01Add primitive floats to 'vm_compute'Guillaume Bertholon
* This commit add float instructions to the VM, their encoding in bytecode and the interpretation of primitive float values after the reduction. * The flag '-std=c99' could be added to the C compiler flags to ensure that float computation strictly follows the norm (ie. i387 80-bits format is not used as an optimization). Actually, we use '-fexcess-precision=standard' instead of '-std=c99' because the latter would disable GNU asm used in the VM.
2019-11-01Add primitive float computation in Coq kernelGuillaume Bertholon
Beware of 0. = -0. issue for primitive floats The IEEE 754 declares that 0. and -0. are treated equal but we cannot say that this is true with Leibniz equality. Therefore we must patch the equality and the total comparison inside the kernel to prevent inconsistency.
2019-10-31Merge PR #10933: Add clarification in make-changelog.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-10-31[Nix] Update reference to nixpkgsVincent Laporte
This version of nixpkgs includes: - Dune 1.11.4 - GTK3 3.24.12 - menhir 20190626
2019-10-30Make changelog script aware of trailing slashes.Arthur Azevedo de Amorim
2019-10-29[declare] Use helper function for `fix_exn` instead of relying on internals.Emilio Jesus Gallego Arias
2019-10-29Merge PR #10892: [engine] Remove UnivGen.global_of_constrPierre-Marie Pédrot
Ack-by: Zimmi48 Reviewed-by: ppedrot
2019-10-29Merge PR #10942: Describe XML tags used for highlighting diff textThéo Zimmermann
Reviewed-by: Zimmi48
2019-10-27Fix link to `coq-notes.md`Michael D. Adams
2019-10-25[funind] Remove duplicate save function.Emilio Jesus Gallego Arias
AFAICT the reasoning for introducing this function doesn't hold anymore. This is needed for future refactorings that should make some types private.
2019-10-24Describe XML tags used for highlighting diff textJim Fehrle
2019-10-18Merge PR #10904: Fix a De Bruijn bug in the computation of term relevance in ↵Gaëtan Gilbert
the kernel. Reviewed-by: SkySkimmer Reviewed-by: Zimmi48 Ack-by: gares
2019-10-17Fix link to `xml-protocol.md` in `dev/README.md`Michael D. Adams
2019-10-16[engine] Remove UnivGen.global_of_constrVincent Laporte
2019-10-16Fix a De Bruijn bug in the computation of term relevance in the kernel.Pierre-Marie Pédrot
Opening up a lambda should always lift the substitution attached to it.
2019-10-14Merge PR #10883: Doc update with mlg extension - fix #10855Jason Gross
Reviewed-by: JasonGross Reviewed-by: gares Ack-by: ppedrot
2019-10-14Merge PR #10811: Allow SProp default onPierre-Marie Pédrot
Reviewed-by: Zimmi48 Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-10-13Doc update with mlg extension - fix #10855mcaci
2019-10-11Merge PR #10828: Simple script to prefill a changelog entryThéo Zimmermann
Reviewed-by: Zimmi48
2019-10-11Merge PR #10850: chmod -x some filesGaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: ppedrot
2019-10-11Simple script to prefill a changelog entryGaëtan Gilbert
2019-10-08Merge PR #10840: Release process: release notesThéo Zimmermann
Reviewed-by: Zimmi48
2019-10-08Merge PR #10770: [ci] Add mit-pdos/perennialEmilio Jesus Gallego Arias
Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: ejgallego
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 07:12:19 +0000