aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Merge PR #6820: Tacticals assert_fails and assert_succeedsGravatar Maxime Dénès2018-03-09
|\
* \ Merge PR #6155: Get rid of ' notation for Zpos in QArithGravatar Maxime Dénès2018-03-09
|\ \
* \ \ Merge PR #6937: Add empty compat file for Coq 8.8Gravatar Maxime Dénès2018-03-09
|\ \ \
* \ \ \ Merge PR #6522: Fix core hint database issue #6521Gravatar Maxime Dénès2018-03-08
|\ \ \ \
* \ \ \ \ Merge PR #6743: Add notation {x & P} for sigTGravatar Maxime Dénès2018-03-08
|\ \ \ \ \
* \ \ \ \ \ Merge PR #6909: Deprecate Focus and UnfocusGravatar Maxime Dénès2018-03-08
|\ \ \ \ \ \
* | | | | | | [stdlib] Do not use “Require” inside sectionsGravatar Vincent Laporte2018-03-07
| | | | * | | Add empty compat file for Coq 8.8Gravatar Jason Gross2018-03-07
| |_|_|/ / / |/| | | | |
* | | | | | Merge PR #6744: Add String.concatGravatar Maxime Dénès2018-03-07
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\ \ \ \ \ \ \
| | | * | | | | Remove all uses of Focus in standard library.Gravatar Théo Zimmermann2018-03-04
* | | | | | | | Remove 8.5 compatibility support.Gravatar Théo Zimmermann2018-03-02
* | | | | | | | Remove VOld compatibility flag.Gravatar Théo Zimmermann2018-03-02
* | | | | | | | Turn warning for deprecated notations on.Gravatar Théo Zimmermann2018-03-02
* | | | | | | | Remove the deprecation for some 8.2-8.5 compatibility aliases.Gravatar Théo Zimmermann2018-03-02
| |_|/ / / / / |/| | | | | |
| | | | | | * Uniform spacing layout in Tactics.v.Gravatar Hugo Herbelin2018-02-28
| | | | | | * Added tacticals assert_succeeds/assert_fails (courtesy of Jason Gross).Gravatar Hugo Herbelin2018-02-28
* | | | | | | Merge PR #6852: [stdlib] move “Require” out of sectionsGravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR #1026: changed statements of Rpower_lt and Rle_power and added lemmasGravatar Maxime Dénès2018-02-28
|\ \ \ \ \ \ \ \
| | | * | | | | | Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| |_|/ / / / / / |/| | | | | | |
| | * | | | | | [stdlib] move “Require” out of sectionsGravatar Vincent Laporte2018-02-27
| |/ / / / / / |/| | | | | |
| | * | | | | Add String.concatGravatar Jason Gross2018-02-24
| |/ / / / / |/| | | | |
* | | | | | Merge PR #6599: Decimals in preludeGravatar Maxime Dénès2018-02-24
|\ \ \ \ \ \ | |_|_|_|_|/ |/| | | | |
* | | | | | Merge PR #6282: proposed fix for issue #3213: extra variable m in Lt.S_predGravatar Maxime Dénès2018-02-21
|\ \ \ \ \ \
| | * | | | | Decimal goodies : conversion to/from Coq stringsGravatar Pierre Letouzey2018-02-20
| | * | | | | Decimal: proofs that conversions from/to nat,N,Z are bijectionsGravatar Pierre Letouzey2018-02-20
| | * | | | | Decimal: simple representation of base-10 numbersGravatar Pierre Letouzey2018-02-20
* | | | | | | Trying a hack to support {'pat|P} without breaking compatibility.Gravatar Hugo Herbelin2018-02-20
* | | | | | | Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc.Gravatar Hugo Herbelin2018-02-20
* | | | | | | More structured printing in unicode notations for binders.Gravatar Hugo Herbelin2018-02-20
* | | | | | | User-level support for Gonthier-Ssreflect's "if t then pat then u else v".Gravatar Hugo Herbelin2018-02-20
| |/ / / / / |/| | | | |
* | | | | | Merge PR #6556: Remove dir-locals and ship suggested helper hooks instead.Gravatar Maxime Dénès2018-02-19
|\ \ \ \ \ \
| | | | * | | Add notation {x & P} for sigTGravatar Tej Chajed2018-02-12
| |_|_|/ / / |/| | | | |
* | | | | | Merge PR #6139: Make list functions returning sumbools transparentGravatar Maxime Dénès2018-02-12
|\ \ \ \ \ \
* | | | | | | Document between and exists_between types.Gravatar Ismail2018-01-08
| | * | | | | Remove dir-locals and ship suggested helper hooks instead.Gravatar Gaëtan Gilbert2018-01-06
| |/ / / / / |/| | | | |
| | | | * | Fix core hint database issue #6521Gravatar Anton Trunov2018-01-03
| |_|_|/ / |/| | | |
* | | | | Fix warning about shadowing a global name.Gravatar Gaëtan Gilbert2017-12-19
* | | | | Add named timers to LtacProfGravatar Jason Gross2017-12-14
* | | | | Merge PR #6335: Additional rewrite lemmas on Ensembles, in Powerset_factsGravatar Maxime Dénès2017-12-12
|\ \ \ \ \
* | | | | | Axiom-free proof of eta expansion.Gravatar Jasper Hugunin2017-12-11
* | | | | | Remove most uses of function extensionality in Program.CombinatorsGravatar Jasper Hugunin2017-12-09
| * | | | | Additional rewrite lemmas on Ensembles, in Powerset_factsGravatar Joachim Breitner2017-12-06
|/ / / / /
| | * | | proposed fix for issue #3213: extra variable m in Lt.S_predGravatar fredokun2017-12-01
* | | | | Fix (partial) #4878: option to stop autodeclaring axiom as instance.Gravatar Gaëtan Gilbert2017-11-28
| |/ / / |/| | |
| * | | Make list functions returning sumbools transparentGravatar Tej Chajed2017-11-15
|/ / /
| | * Get rid of ' notation for Zpos in QArith.Gravatar Robbert Krebbers2017-11-14
| |/ |/|
* | Merge PR #1113: Adding 3 Arith/QArith lemmas that I found usefulGravatar Maxime Dénès2017-10-27
|\ \
| * | Chaining two tactics in a proofGravatar Raphaël Monat2017-10-27
| * | Moving from `is_true` to `= true`Gravatar Raphaël Monat2017-10-25