| Age | Commit message (Expand) | Author |
|---|
| 2019-11-27 | [release] Update files for 8.12 release per release process. | Emilio Jesus Gallego Arias |
| 2019-11-11 | Run update-compat script with --release option. | Théo Zimmermann |
| 2019-11-01 | Merge PR #10022: [ssr] Generalize tactics under and over to any (Reflexive) r... | Enrico Tassi |
| 2019-11-01 | docs: Add refman+stdlib documentation | Erik Martin-Dorel |
| 2019-10-27 | Merge PR #10827: Replace classical reals quotient axioms by functional extens... | Hugo Herbelin |
| 2019-10-24 | Replace classical reals quotient axioms by functional extensionality. Define ... | Vincent Semeria |
| 2019-10-07 | Call to update-compat.py. | Pierre-Marie Pédrot |
| 2019-09-16 | Define morphisms of real numbers and accelerate Cauchy reals | Vincent Semeria |
| 2019-08-19 | Split ConstructiveRealsLUB and improve comments | Vincent Semeria |
| 2019-08-08 | Add interface of constructive real numbers, with an opaque implementation by ... | Vincent Semeria |
| 2019-08-08 | [ssr] Refactor under's Setoid generalization to ease stdlib2 porting | Erik Martin-Dorel |
| 2019-08-05 | Merge PR #10445: Split constructive and classical axioms for real numbers | Vincent Laporte |
| 2019-07-26 | [stdlib] Remove deprecated module Zsqrt_compat | Vincent Laporte |
| 2019-07-26 | [stdlib] Remove deprecated module Zlogarithm | Vincent Laporte |
| 2019-07-17 | Rename ConstructiveRIneq and ConstructiveRcomplete | Vincent Semeria |
| 2019-07-16 | Define constructive real numbers as Cauchy sequences of rational numbers. Red... | Vincent Semeria |
| 2019-04-02 | Remove -compat 8.7 | Jason Gross |
| 2019-03-14 | Add StrictProp.v with basic SProp related definitions | Gaëtan Gilbert |
| 2019-02-04 | Primitive integers | Maxime Dénès |
| 2019-01-24 | Update -compat to support -compat 8.10 | Jason Gross |
| 2018-11-28 | Add `String Notation` vernacular like `Numeral Notation` | Jason Gross |
| 2018-11-16 | Merge PR #8888: Proof runcountable rebase | Hugo Herbelin |
| 2018-11-07 | [doc] also scan plugins/ to build the lirbary index | Enrico Tassi |
| 2018-11-01 | Fix header and doc index | Vincent Semeria |
| 2018-10-17 | doc: mention ByteVector | Yishuai Li |
| 2018-10-02 | Update the -compat flags | Jason Gross |
| 2018-08-31 | Numeral Notation for nat | Pierre Letouzey |
| 2018-07-16 | bin,oct,hex conversions positive,Z,N,nat<->string | Jason Gross |
| 2018-03-07 | Add empty compat file for Coq 8.8 | Jason Gross |
| 2018-03-02 | Remove 8.5 compatibility support. | Théo Zimmermann |
| 2018-02-20 | Doc: add Decimal-related files to index-list.html.template | Jason Gross |
| 2017-07-21 | Adding a V8.7 compatibility version number. | Hugo Herbelin |
| 2017-06-14 | Remove support for Coq 8.4. | Guillaume Melquiond |
| 2017-06-13 | BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo) | Pierre Letouzey |
| 2017-03-03 | Adding explicitly a file to work in the context of propositional extensionality. | Hugo Herbelin |
| 2017-03-03 | Adding a file providing extensional choice (i.e. choice over setoids). | Hugo Herbelin |
| 2017-03-03 | Logic library: Adding a characterization of excluded-middle in term of | Hugo Herbelin |
| 2016-07-06 | Fix #4793: Coq 8.6 should accept -compat 8.6 | Maxime Dénès |
| 2016-06-03 | Fix build of documentation (broken for four months). | Guillaume Melquiond |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-13 | MMaps: remove it from final 8.5 release, since this new library isn't mature ... | Pierre Letouzey |
| 2015-12-15 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2015-12-14 | Moved proof_admitted to its own file, named "AdmitAxiom.v". | Maxime Dénès |
| 2015-11-07 | Adding an amazing property of Prop. | Hugo Herbelin |
| 2015-10-02 | Mark the Coq.Compat files for documentation. (Fix bug #4353) | Guillaume Melquiond |
| 2015-04-02 | Fix compilation of documentation broken by the addition of MMapAVL. | Guillaume Melquiond |
| 2015-03-21 | Index MMaps files, otherwise documentation cannot be built. (Fix for bug #4107) | Guillaume Melquiond |
| 2014-12-09 | doc/stdlib: fix the xhtml validity of the index-list template | Pierre Letouzey |
| 2014-12-09 | Port to trunk the old commit r14895 of v8.4 (styles for the stdlib documentat... | notin |
| 2014-07-15 | Added a (constructive) proof of Weak Konig's lemma for decidable trees. | Hugo Herbelin |
