| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2019-11-07 | Merge PR #11059: Swap parsing precedence of `::` and `,` ; Fix #10116 | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2019-11-06 | Merge PR #11038: fix(*.opam): Add missing version "dev" | Emilio Jesus Gallego Arias | |
| Reviewed-by: Zimmi48 | |||
| 2019-11-06 | Swap parsing precedence of `::` and `,` ; Fix #10116 | Kenji Maillard | |
| 2019-11-06 | Merge PR #11041: Cite POPL19 SProp paper | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
| 2019-11-06 | Merge PR #11051: elpi 1.8 | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer Reviewed-by: ejgallego | |||
| 2019-11-05 | overlay | Enrico Tassi | |
| 2019-11-05 | elpi 1.8 | Enrico Tassi | |
| 2019-11-04 | Cite POPL19 SProp paper | Gaëtan Gilbert | |
| Close #10242 | |||
| 2019-11-04 | fix(*.opam): Add missing version | Erik Martin-Dorel | |
| "dev" was not implied, and this can cause the following issues: --8<---------------cut here---------------start------------->8--- $ docker run --rm -it coqorg/base:latest coq@…:~$ opam update coq@…:~$ git clone https://github.com/coq/coq.git Cloning into 'coq'... coq@…:~$ cd coq coq@…:~/coq$ opam pin add -n -k path coq . [coq.8.10.1] synchronised from file:///home/coq/coq coq is now pinned to file:///home/coq/coq (version 8.10.1) # issue 1. opam picks the first version he finds for coq from repos… coq@…:~/coq$ mv coq.opam foo.opam coq@…:~/coq$ opam pin add -n -k path foo . Package foo does not exist, create as a NEW package? [Y/n] y [foo.~dev] synchronised from file:///home/coq/coq foo is now pinned to file:///home/coq/coq (version ~dev) # issue 2. if none is found, opam sticks to some "~dev" version… --8<---------------cut here---------------end--------------->8--- | |||
| 2019-11-03 | Merge PR #10958: Elan → Stratego in documentation of `rewrite_strat`. | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
| 2019-11-03 | Elan → Stratego in documentation of `rewrite_strat`. | Robbert Krebbers | |
| @eelcovisser told me that the strategies in Luttik and Visser 97 were inspired by Elan, but they are not part of Elan. They are part of the Stratego language. | |||
| 2019-11-02 | Merge PR #11007: [classes] Some refactoring on proof save preparation. | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer | |||
| 2019-11-01 | Merge PR #11028: Update the deprecation doc of `Shrink Obligations` | Clément Pit-Claudel | |
| 2019-11-01 | Merge PR #10647: Expose universe processing in comInductive. | Gaëtan Gilbert | |
| Reviewed-by: SkySkimmer Reviewed-by: ppedrot | |||
| 2019-11-01 | Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) ↵ | Enrico Tassi | |
| relation Reviewed-by: gares | |||
| 2019-11-01 | Update the deprecation doc of `Shrink Obligations` | Jason Gross | |
| Now it uses `.. deprecated` like all the other deprecation notices in the manual. | |||
| 2019-11-01 | Merge 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-01 | minor cleanup of anonymous functions | Gaëtan Gilbert | |
| 2019-11-01 | Expose universe processing in comInductive. | Jan-Oliver Kaiser | |
| 2019-11-01 | Merge PR #8642: Compiled interfaces with -vos and -vok options | Pierre-Marie Pédrot | |
| Ack-by: SkySkimmer Ack-by: Zimmi48 Ack-by: ejgallego Ack-by: gares Ack-by: maximedenes Ack-by: ppedrot | |||
| 2019-11-01 | Merge PR #11019: enforcing Ltac2 constructor name are uppercased | Pierre-Marie Pédrot | |
| Reviewed-by: ppedrot | |||
| 2019-11-01 | adding test file for Uppercase Ltac2 constructors | Kenji Maillard | |
| 2019-11-01 | enforcing Ltac2 cosntructors name are uppercase in open types | Kenji Maillard | |
| 2019-11-01 | Add warnings regarding the experimental nature of the vos feature in the doc. | Pierre-Marie Pédrot | |
| 2019-11-01 | Teach coq_dune about the empty .vos produced by coqc | Gaëtan Gilbert | |
| Without this the next dune command after build a vo will wipe out the vos, breaking interactive users. Also this means dune installs the .vos files. | |||
| 2019-11-01 | [test-suite] acknowledge coq_mafile installs .vos | Enrico Tassi | |
| 2019-11-01 | [make] install .vos along with .vo | Enrico Tassi | |
| 2019-11-01 | fix installation of vos files in coq Makefile | charguer | |
| 2019-11-01 | a tentative patch to allow interactive session to load .vos files; (recall ↵ | charguer | |
| that the generation of a .vo files induces the creation of an empty .vos file.) | |||
| 2019-11-01 | fix coq_makefile and doc for vos support. | charguer | |
| 2019-11-01 | Changelog entry | Maxime Dénès | |
| 2019-11-01 | additional details in the doc for -vos | charguer | |
| 2019-11-01 | Implementing support for vos/vok files. | charguer | |
| A .vos file stores the result of compiling statements (defs, lemmas) but not proofs. A .vok file is an empty file that denotes successful compilation of the full contents of a .v file. Unlike a .vio file, a .vos file does not store suspended proofs, so it is more lightweight. It cannot be completed into a .vo file. | |||
| 2019-11-01 | Merge PR #11015: [Nix] Update reference to nixpkgs | Théo Zimmermann | |
| Reviewed-by: Zimmi48 | |||
| 2019-11-01 | docs(gallina-extensions.rst): Say more on float literals extraction | Erik Martin-Dorel | |
| 2019-11-01 | Communicate CFLAGS to dune | Pierre Roux | |
| 2019-11-01 | Add some doc snippet in ExtrOCamlFloats.v | Erik Martin-Dorel | |
| (as suggested by @silene) | |||
| 2019-11-01 | Makefile.build: Fix rules of bin/votour{,.byte} | Erik Martin-Dorel | |
| 2019-11-01 | Add extraction for primitive floats | Erik Martin-Dorel | |
| Co-authored-by: Pierre Roux <pierre.roux@onera.fr> | |||
| 2019-11-01 | Add a check for gradual underflows | Pierre Roux | |
| 2019-11-01 | Add the IEEE-754 arch requirement in INSTALL | Pierre Roux | |
| Co-authored-by: Erik Martin-Dorel <erik.martin-dorel@irit.fr> | |||
| 2019-11-01 | feat: Use SSE2_MATH if available & Die if missing on x87 | Erik Martin-Dorel | |
| Co-authored-by: Pierre Roux <pierre.roux@onera.fr> | |||
| 2019-11-01 | Fix ldshiftexp | Pierre Roux | |
| * Fix the implementations and add tests * Change shift from int63 to Z (was always used as a Z) * Update FloatLemmas.v accordingly Co-authored-by: Erik Martin-Dorel <erik.martin-dorel@irit.fr> | |||
| 2019-11-01 | Add overlays | Pierre Roux | |
| 2019-11-01 | docs: Add entry in changelog | Erik Martin-Dorel | |
| 2019-11-01 | docs: Add refman+stdlib documentation | Erik Martin-Dorel | |
| 2019-11-01 | Add "==", "<", "<=" in PrimFloat.v | Erik Martin-Dorel | |
| * Add a related test-suite in compare.v (generated by a bash script) Co-authored-by: Pierre Roux <pierre.roux@onera.fr> | |||
| 2019-11-01 | Make primitive float work on Windows | Pierre Roux | |
| 2019-11-01 | Reimplement is_float | Pierre Roux | |
| is_float was relying on Obj.tag triggering a check that we are in the OCaml heap which is expensive. On extreme examples, this can lead to a global 2x speedup. Thanks to Maxime Dénès and Jacques-Henri Jourdan for their help in diagnosing this. | |||
| 2019-11-01 | Make primitive float work on x86_32 | Pierre Roux | |
| Flag -fexcess-precision=standard is not enough on x86_32 where -msse2 -mfpmath=sse is required (-msse is not enough) to avoid double rounding issues in the VM. Most floating-point operation are now implemented in C because OCaml is suffering double rounding issues on x86_32 with 80 bits extended precision registers used for floating-point values, causing double rounding making floating-point arithmetic incorrect with respect to its specification. Add a runtime test for double roundings. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |