| Age | Commit message (Expand) | Author |
|---|
| 2018-07-10 | Fix typo in Init.Logic. | whitequark |
| 2018-07-02 | hints: add Hint Variables/Constants Opaque/Transparent commands | Matthieu Sozeau |
| 2018-03-09 | Merge PR #6820: Tacticals assert_fails and assert_succeeds | Maxime Dénès |
| 2018-03-08 | Merge PR #6522: Fix core hint database issue #6521 | Maxime Dénès |
| 2018-03-08 | Merge PR #6743: Add notation {x & P} for sigT | Maxime Dénès |
| 2018-03-05 | Merge PR #6855: Update headers following #6543. | Maxime Dénès |
| 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-27 | Update headers following #6543. | Théo Zimmermann |
| 2018-02-24 | Merge PR #6599: Decimals in prelude | Maxime Dénès |
| 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 | User-level support for Gonthier-Ssreflect's "if t then pat then u else v". | Hugo Herbelin |
| 2018-02-12 | Add notation {x & P} for sigT | Tej Chajed |
| 2018-01-03 | Fix core hint database issue #6521 | Anton Trunov |
| 2017-12-14 | Add named timers to LtacProf | Jason Gross |
| 2017-10-19 | Moving bug numbers to BZ# format in the source code. | Théo Zimmermann |
| 2017-08-29 | A little reorganization of notations + a fix to #5608. | Hugo Herbelin |
| 2017-07-05 | Fix typo in documentation for identity | Tej Chajed |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot |
| 2017-06-15 | plugins/ltac : avoid spurious .cmxs files | Pierre Letouzey |
| 2017-06-14 | Prelude : no more autoload of plugins extraction and recdef | Pierre Letouzey |
| 2017-06-13 | Merge PR#385: Equality of sigma types | Maxime Dénès |
| 2017-06-01 | drop vo.itarget files and compute the corresponding the corresponding values ... | Matej Kosik |
| 2017-05-28 | More uniform indentation of sigma lemmas | Jason Gross |
| 2017-05-28 | Give explicit proof terms to proj2_sig_eq etc. | Jason Gross |
| 2017-05-28 | Use the rew dependent notation in ex, ex2 proofs | Jason Gross |
| 2017-05-28 | Make theorems about ex equality Qed | Jason Gross |
| 2017-05-28 | Make new proofs of equality Qed | Jason Gross |
| 2017-05-28 | Add some more comments about sigma equalities | Jason Gross |
| 2017-05-28 | Remove motive argument from [rew dependent] | Jason Gross |
| 2017-05-28 | Use a local [rew dependent] notation | Jason Gross |
| 2017-05-28 | Add forward-chaining versions: [eq_sig*_uncurried] | Jason Gross |
| 2017-05-28 | Use notation for sigT | Jason Gross |
| 2017-05-28 | Remove reference to [IsIso] | Jason Gross |
| 2017-05-28 | Use notations for [sig], [sigT], [sig2], [sigT2] | Jason Gross |
| 2017-05-28 | Use extended notation for ex, ex2 types | Jason Gross |
| 2017-05-28 | Replace [ex'] with [ex] | Jason Gross |
| 2017-05-28 | Use [rew_] instead of [eq_rect_] prefix | Jason Gross |
| 2017-05-28 | Add equality lemmas for sig2 and sigT2 | Jason Gross |
| 2017-05-28 | Add lemmas for ex2 | Jason Gross |
| 2017-05-28 | Use [rew] notations rather than [eq_rect] | Jason Gross |
| 2017-05-28 | Add an [inversion_sigma] tactic | Jason Gross |
| 2017-05-28 | Add lemmas about equality of sigma types | Jason Gross |
| 2017-05-28 | Use [rew_] instead of [eq_rect_] prefix | Jason Gross |
| 2017-05-28 | Use [rew] notations rather than [eq_rect] | Jason Gross |
| 2017-05-28 | Add more groupoid-like theorems about [eq] | Jason Gross |
