| Age | Commit message (Expand) | Author |
|---|
| 2018-03-02 | Turn warning for deprecated notations on. | Théo Zimmermann |
| 2018-03-02 | Remove the deprecation for some 8.2-8.5 compatibility aliases. | Théo Zimmermann |
| 2018-02-28 | Uniform spacing layout in Tactics.v. | Hugo Herbelin |
| 2018-02-28 | Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross). | Hugo Herbelin |
| 2018-02-28 | Merge PR #6852: [stdlib] move “Require” out of sections | Maxime Dénès |
| 2018-02-28 | Merge PR #1026: changed statements of Rpower_lt and Rle_power and added lemmas | Maxime Dénès |
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann |
| 2018-02-27 | [stdlib] move “Require” out of sections | Vincent Laporte |
| 2018-02-24 | Add String.concat | Jason Gross |
| 2018-02-24 | Merge PR #6599: Decimals in prelude | Maxime Dénès |
| 2018-02-21 | Merge PR #6282: proposed fix for issue #3213: extra variable m in Lt.S_pred | Maxime Dénès |
| 2018-02-20 | Decimal goodies : conversion to/from Coq strings | Pierre Letouzey |
| 2018-02-20 | Decimal: proofs that conversions from/to nat,N,Z are bijections | Pierre Letouzey |
| 2018-02-20 | Decimal: simple representation of base-10 numbers | Pierre Letouzey |
| 2018-02-20 | Trying a hack to support {'pat|P} without breaking compatibility. | Hugo Herbelin |
| 2018-02-20 | Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc. | Hugo Herbelin |
| 2018-02-20 | More structured printing in unicode notations for binders. | Hugo Herbelin |
| 2018-02-20 | User-level support for Gonthier-Ssreflect's "if t then pat then u else v". | Hugo Herbelin |
| 2018-02-19 | Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead. | Maxime Dénès |
| 2018-02-12 | Add notation {x & P} for sigT | Tej Chajed |
| 2018-02-12 | Merge PR #6139: Make list functions returning sumbools transparent | Maxime Dénès |
| 2018-01-08 | Document between and exists_between types. | Ismail |
| 2018-01-06 | Remove dir-locals and ship suggested helper hooks instead. | Gaëtan Gilbert |
| 2018-01-03 | Fix core hint database issue #6521 | Anton Trunov |
| 2017-12-19 | Fix warning about shadowing a global name. | Gaëtan Gilbert |
| 2017-12-14 | Add named timers to LtacProf | Jason Gross |
| 2017-12-12 | Merge PR #6335: Additional rewrite lemmas on Ensembles, in Powerset_facts | Maxime Dénès |
| 2017-12-11 | Axiom-free proof of eta expansion. | Jasper Hugunin |
| 2017-12-09 | Remove most uses of function extensionality in Program.Combinators | Jasper Hugunin |
| 2017-12-06 | Additional rewrite lemmas on Ensembles, in Powerset_facts | Joachim Breitner |
| 2017-12-01 | proposed fix for issue #3213: extra variable m in Lt.S_pred | fredokun |
| 2017-11-28 | Fix (partial) #4878: option to stop autodeclaring axiom as instance. | Gaëtan Gilbert |
| 2017-11-15 | Make list functions returning sumbools transparent | Tej Chajed |
| 2017-11-14 | Get rid of ' notation for Zpos in QArith. | Robbert Krebbers |
| 2017-10-27 | Merge PR #1113: Adding 3 Arith/QArith lemmas that I found useful | Maxime Dénès |
| 2017-10-27 | Chaining two tactics in a proof | Raphaël Monat |
| 2017-10-25 | Moving from `is_true` to `= true` | Raphaël Monat |
| 2017-10-19 | Moving bug numbers to BZ# format in the source code. | Théo Zimmermann |
| 2017-10-12 | Added proofs of Qeq_bool_refl, Qeq_bool_sym, Qeq_bool_trans. | Raphaël Monat |
| 2017-10-10 | Merge PR #768: Omega and romega know about context definitions (fix old bug 148) | Maxime Dénès |
| 2017-10-08 | Changed Qeq_bool_sym into Qeq_bool_comm, used the proof of @letouzey. | Raphaël Monat |
| 2017-10-08 | Removed leb_not_le (already existing as Nat.leb_nle) | Raphaël Monat |
| 2017-10-07 | Compat/Coq87.v : Unset Omega UseLocalDefs (see PR #768) | Pierre Letouzey |
| 2017-10-05 | [ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms. | Emilio Jesus Gallego Arias |
| 2017-10-03 | Changed the statement of leb_not_le; shortened the proof | Raphaël Monat |
| 2017-10-03 | Add Qabs_Qinv: Qabs (/ q) == / (Qabs q). | Raphaël Monat |
| 2017-10-03 | Add Qeq_bool_sym: Qeq_bool x y = Qeq_bool y x. | Raphaël Monat |
| 2017-10-03 | Add leb_not_le: (n <=? m) = false -> n > m. | Raphaël Monat |
| 2017-09-15 | Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" work... | Maxime Dénès |
| 2017-09-06 | weakens an hypothesis of Rle_Rpower | Yves Bertot |
