aboutsummaryrefslogtreecommitdiff
path: root/dev
AgeCommit message (Collapse)Author
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
2019-10-07chmod -x some filesJason Gross
They probably don't need to be executable
2019-10-07Release process: release notesVincent Laporte
Explain into the release process how to prepare the release notes.
2019-10-07Merge PR #9933: Add a few missing notes to the release doc.Vincent Laporte
Ack-by: ejgallego Reviewed-by: vbgl
2019-10-04overlays for sprop default onGaëtan Gilbert
2019-10-03Merge PR #10727: [library] Move `Declaremods` to `vernac/`Pierre-Marie Pédrot
Ack-by: SkySkimmer Reviewed-by: herbelin Reviewed-by: ppedrot
2019-10-02Merge PR #10768: [ci] Update to OCaml 4.09.0, drop now useless "trunk" jobs.Gaëtan Gilbert
Reviewed-by: SkySkimmer Reviewed-by: Zimmi48
2019-09-25Adding documentation for the move of sections data to kernel.Pierre-Marie Pédrot
2019-09-20[ci] Add mit-pdos/perennialTej Chajed
2019-09-19[ci] Update supported OCaml version to 4.09.0Emilio Jesus Gallego Arias
2019-09-18[declaremods] Remove abstraction layer over module interpretation.Emilio Jesus Gallego Arias
Now that we place imperative module declaration on top of module interpretation we can remove the abstraction layer used in `Declaremods`, so the `interp_modast` parameter goes away. Improvement suggested by Gaëtan Gilbert.
2019-09-17Merge PR #10738: update elpi to 1.7Gaëtan Gilbert
Reviewed-by: SkySkimmer
2019-09-17Overlay for VSTMaxime Dénès
2019-09-16Add SF overlayMaxime Dénès
2019-09-07overlay for elpiEnrico Tassi
2019-09-07update elpi to 1.7Enrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 02:27:20 +0000