aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
2020-01-03Merge PR #11295: Use code owner teams for every component.Maxime Dénès
Reviewed-by: maximedenes
2019-12-31Merge PR #11338: Remove uses of Global in Evd API.Gaëtan Gilbert
Reviewed-by: ejgallego Reviewed-by: herbelin
2019-12-28Merge PR #11323: Fix mulc on 32-bit architecturesMichael Soegtrop
Reviewed-by: MSoegtropIMC
2019-12-27Add critical-bugs entry, tests-suite file, and code comment.Guillaume Melquiond
2019-12-26Remove uses of Global in Evd API.Pierre-Marie Pédrot
Namely, Evd.evar_env and Evd.evar_filtered_env now take an additional environment instead of querying the imperative global one. We percolate this change as higher up as possible.
2019-12-24Update merging doc following the full move to teams.Théo Zimmermann
Integrate merging doc in the main contributing document.
2019-12-24Merge PR #11316: Windows: switch OCaml to 4.08.1Emilio Jesus Gallego Arias
Reviewed-by: ejgallego
2019-12-23Windows: switch OCaml to 4.08.1Michael Soegtrop
- remove manual flexlink circular dependency handling - use standard configure process instead of hand made windows make files - enable parallel build - remove bootstrapping step (maybe should be there for release builds)
2019-12-22Rename files with Class in their name to make their role clearer.Pierre-Marie Pédrot
We restrict to those that are actually related to typeclasses, and perform the following renamings: Classops --> Coercionops Class --> ComCoercion
2019-12-18Merge PR #9786: Fix Equation's ci scriptPierre-Marie Pédrot
Reviewed-by: ejgallego Reviewed-by: ppedrot
2019-12-16Overlay for #11027Gaëtan Gilbert
2019-12-13Merge PR #11259: [make] Rename Makefile to Makefile.make and INSTALL to ↵Théo Zimmermann
INSTALL.md Ack-by: SkySkimmer Reviewed-by: Zimmi48 Reviewed-by: gares Ack-by: jfehrle
2019-12-13Add ocamlformat dependency to Nix fileMaxime Dénès
2019-12-13[doc] [INSTALL] split make-based install instructions to its own file.Emilio Jesus Gallego Arias
2019-12-13[doc] [INSTALL] Port INSTALL to markdown format.Emilio Jesus Gallego Arias
2019-12-13[fmt] [dune] Add ocamlformat configuration.Emilio Jesus Gallego Arias
For now we don't enable it in any source file, neither on dune files. `lint-repository` has been updated so it will check `dune build @fmt` returns 0.
2019-12-13[ci] [docker] Install ocamlformat in docker images.Emilio Jesus Gallego Arias
2019-12-13Fix Equation's ci scriptMatthieu Sozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 22:56:06 +0000