| Commit message (Expand) | Author | Age |
* | Merge PR #6855: Update headers following #6543. | Maxime Dénès | 2018-03-05 |
|\ |
|
* | | Remove 8.5 compatibility support. | Théo Zimmermann | 2018-03-02 |
* | | Remove VOld compatibility flag. | Théo Zimmermann | 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-03-02 |
* | | 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-28 |
|\ \ \ |
|
| | | * | Update headers following #6543. | Théo Zimmermann | 2018-02-27 |
| |_|/
|/| | |
|
| | * | [stdlib] move “Require” out of sections | Vincent Laporte | 2018-02-27 |
| |/
|/| |
|
* | | Merge PR #6599: Decimals in prelude | Maxime Dénès | 2018-02-24 |
|\ \ |
|
* \ \ | Merge PR #6282: proposed fix for issue #3213: extra variable m in Lt.S_pred | Maxime Dénès | 2018-02-21 |
|\ \ \ |
|
| | * | | 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-20 |
| |/ /
|/| | |
|
* | | | Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead. | Maxime Dénès | 2018-02-19 |
|\ \ \ |
|
* \ \ \ | Merge PR #6139: Make list functions returning sumbools transparent | Maxime Dénès | 2018-02-12 |
|\ \ \ \ |
|
* | | | | | Document between and exists_between types. | Ismail | 2018-01-08 |
| | * | | | Remove dir-locals and ship suggested helper hooks instead. | Gaëtan Gilbert | 2018-01-06 |
| |/ / /
|/| | | |
|
* | | | | Fix warning about shadowing a global name. | Gaëtan Gilbert | 2017-12-19 |
* | | | | Add named timers to LtacProf | Jason Gross | 2017-12-14 |
* | | | | Merge PR #6335: Additional rewrite lemmas on Ensembles, in Powerset_facts | Maxime Dénès | 2017-12-12 |
|\ \ \ \ |
|
* | | | | | Axiom-free proof of eta expansion. | Jasper Hugunin | 2017-12-11 |
* | | | | | Remove most uses of function extensionality in Program.Combinators | Jasper Hugunin | 2017-12-09 |
| * | | | | Additional rewrite lemmas on Ensembles, in Powerset_facts | Joachim Breitner | 2017-12-06 |
|/ / / / |
|
| | * | | proposed fix for issue #3213: extra variable m in Lt.S_pred | fredokun | 2017-12-01 |
* | | | | Fix (partial) #4878: option to stop autodeclaring axiom as instance. | Gaëtan Gilbert | 2017-11-28 |
| |/ /
|/| | |
|
| * | | Make list functions returning sumbools transparent | Tej Chajed | 2017-11-15 |
|/ / |
|
* | | 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-27 |
| * | | Moving from `is_true` to `= true` | Raphaël Monat | 2017-10-25 |
* | | | Moving bug numbers to BZ# format in the source code. | Théo Zimmermann | 2017-10-19 |
| * | | Added proofs of Qeq_bool_refl, Qeq_bool_sym, Qeq_bool_trans. | Raphaël Monat | 2017-10-12 |
* | | | Merge PR #768: Omega and romega know about context definitions (fix old bug 148) | Maxime Dénès | 2017-10-10 |
|\ \ \ |
|
| | * | | 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-08 |
| * | | | Compat/Coq87.v : Unset Omega UseLocalDefs (see PR #768) | Pierre Letouzey | 2017-10-07 |
* | | | | [ltac] Warning for deprecated `Add Setoid` and `Add Morphism` forms. | Emilio Jesus Gallego Arias | 2017-10-05 |
|/ / / |
|
| * | | 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-10-03 |
|/ / |
|
* | | Merge PR #986: Ensuring all .v files end with a newline to make "sed -i" work... | Maxime Dénès | 2017-09-15 |
|\ \ |
|
| | * | weakens an hypothesis of Rle_Rpower | Yves Bertot | 2017-09-06 |
| | * | changed statements of Rpower_lt and Rle_power and added | Yves Bertot | 2017-09-06 |
* | | | Addressing BZ#5713 (classical_left/classical_right artificially restricted). | Hugo Herbelin | 2017-09-03 |
| |/
|/| |
|
* | | A little reorganization of notations + a fix to #5608. | Hugo Herbelin | 2017-08-29 |