| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 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 |
| 2017-05-11 | Merge PR#201: Transparent abstract | Maxime Dénès |
| 2017-05-05 | Merge PR#605: Report a useful error for dependent induction | Maxime Dénès |
| 2017-05-05 | Merge PR#593: Functional choice <-> [inhabited] and [forall] commute | Maxime Dénès |
| 2017-05-03 | Report a useful error for dependent induction | Tej Chajed |
| 2017-04-30 | Functional choice <-> [inhabited] and [forall] commute | Gaetan Gilbert |
| 2017-04-28 | Add .dir-locals.el and _CoqProject files for emacs stdlib editing | Jason Gross |
| 2017-04-27 | Merge PR#584: Give andb_prop a simpler proof | Maxime Dénès |
| 2017-04-26 | Small typo in comment | Vadim Zaliva |
| 2017-04-25 | Add transparent_abstract tactic | Jason Gross |
| 2017-04-25 | Give andb_prop a simpler proof | Jason Gross |
| 2017-04-15 | Merge branch 'v8.6' into trunk | Maxime Dénès |
| 2017-04-06 | Merge PR#455: Farewell decl_mode | Maxime Dénès |
