| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2021-04-01 | changelog for 8.13.2 | Enrico Tassi | |
| 2021-03-26 | Document as critical. | Guillaume Melquiond | |
| 2021-03-26 | Adding a changelog. | Pierre-Marie Pédrot | |
| 2021-02-26 | Delay the dynamic linking of native-code libraries until native_compute is ↵ | Guillaume Melquiond | |
| called (fix #13849). The libraries are eventually linked in native_norm and native_conv_gen, just before mk_norm_code and mk_conv_code are called. This commit also renames call_linker as execute_library to better reflect its role. It also makes link_library independent from it, since their error handling are completely opposite. | |||
| 2021-02-22 | changelog for 8.13.1 | Enrico Tassi | |
| 2021-02-20 | Update doc/changelog/01-kernel/13867-changelog-for-13867.rst | Enrico Tassi | |
| Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com> | |||
| 2021-02-20 | add changelog for 13867 | Enrico Tassi | |
| 2021-01-04 | Document the change of case representation. | Pierre-Marie Pédrot | |
| 2020-12-06 | [doc] update changes after 13501 | Enrico Tassi | |
| 2020-12-03 | [changelog] update markup | Enrico Tassi | |
| 2020-12-03 | Changes for Coq 8.13 | Matthieu Sozeau | |
| 2020-11-27 | [kernel] Fix #13495: incompleteness in cases typing for cumulative inductive ↵ | Matthieu Sozeau | |
| types | |||
| 2020-11-13 | Make the universe of primitive arrays irrelevant | Gaëtan Gilbert | |
| Fix #13354 This change is very specific to array, but should not be a significant obstacle to generalization of the feature to eg axioms if we want to later. | |||
| 2020-11-05 | Changelog for 8.12.1. | Théo Zimmermann | |
| 2020-08-18 | Fix subject reduction VS cumulative inductives and function eta | Gaëtan Gilbert | |
| Fix #7015 | |||
| 2020-07-08 | Adding change log. | Hugo Herbelin | |
| 2020-07-06 | Primitive persistent arrays | Maxime Dénès | |
| Persistent arrays expose a functional interface but are implemented using an imperative data structure. The OCaml implementation is based on Jean-Christophe Filliâtre's. Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr> Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | |||
| 2020-07-01 | UIP in SProp | Gaëtan Gilbert | |
| 2020-05-14 | Add a changelog for 8.11.2. | Pierre-Marie Pédrot | |
| 2020-04-13 | Fix #11783 Require in Section | Gaëtan Gilbert | |
| 2020-04-03 | Adding changelog for 8.11.1. | Pierre-Marie Pédrot | |
| 2020-03-12 | Add changelog entry | SimonBoulier | |
| 2020-01-22 | Move new entries in 8.11.0 changelog. | Théo Zimmermann | |
| 2020-01-22 | Changelog for 8.11.0. | Théo Zimmermann | |
| 2020-01-22 | Fix #11421 computation of Set+2 | Gaëtan Gilbert | |
| 2020-01-13 | Native compute: cleanup temporary files on program exit | Gaëtan Gilbert | |
| We make a temporary directory for these files and cleanup at process exit. The temporary directory means we don't have to guess what extensions ocaml will produce, we can just delete everything there. We use Lazy to avoid spamming unused directories when ahead-of-time compiling without actually using native casts / nativenorm (typically stdlib files). Sadly ocaml has "create temp file" but not "create temp dir", so we have to copy the name generation code. Fix #10495 | |||
| 2020-01-06 | Fix #11360: discharge of template inductive with param only use of var | Gaëtan Gilbert | |
| 2019-12-02 | Move unreleased changelog to new 8.11 section. | Théo Zimmermann | |
| 2019-11-28 | [changelog] Add types to changelog entries. | Théo Zimmermann | |
| Types of changes are defined in the list defined by Keep a Changelog 1.0.0 (https://keepachangelog.com/en/1.0.0/): - Added - Changed - Deprecated - Fixed - Removed We exclude the type Security for now, even for soundness fixes, because the process of handling security vulnerabilities is different from anything we follow right now. | |||
| 2019-11-28 | Fix extension of changelog file. | Théo Zimmermann | |
| 2019-11-01 | docs: Add entry in changelog | Erik Martin-Dorel | |
| 2019-10-24 | Release notes for Coq 8.10.1 | Vincent Laporte | |
| 2019-10-16 | Fix 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-05 | Changelog for SProp on | Gaëtan Gilbert | |
| 2019-09-25 | Adding documentation for the move of sections data to kernel. | Pierre-Marie Pédrot | |
| 2019-09-12 | Release notes for 8.10+beta3. | Théo Zimmermann | |
| 2019-08-26 | Document `Template Check` flag and add changelog entry for 9918 | Matthieu Sozeau | |
| Fix changelog entry Fix build of the user manual Markup fixes from Théo Zimmermann Update doc and changelog and improve error messages. | |||
| 2019-07-08 | Adding a changelog. | Pierre-Marie Pédrot | |
| 2019-05-05 | Create categories in changelog. | Théo Zimmermann | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |