| 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-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-27 | Update headers following #6543. | Théo Zimmermann |
| 2018-02-20 | Adding notations of the form "{'pat|P}", "exists2 'pat, P & Q", etc. | Hugo Herbelin |
| 2017-07-04 | Bump year in headers. | Pierre-Marie Pédrot |
| 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 | 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 lemmas for ex2 | Jason Gross |
| 2017-05-28 | Use [rew] notations rather than [eq_rect] | 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-04-30 | Functional choice <-> [inhabited] and [forall] commute | Gaetan Gilbert |
| 2017-04-26 | Small typo in comment | Vadim Zaliva |
| 2017-04-15 | Merge branch 'v8.6' into trunk | Maxime Dénès |
| 2017-03-17 | Merge PR#442: Allow interactive editing of Coq.Init.Logic | Maxime Dénès |
| 2017-03-03 | Compatibility of iff wrt not and imp. | Hugo Herbelin |
| 2017-02-23 | Fixing a little bug in printing ex2 (type was printed "_" by default). | Hugo Herbelin |
| 2017-02-21 | Allow interactive editing of Coq.Init.Logic | Jason Gross |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2015-10-02 | Remove Print Universe directive. | Matthieu Sozeau |
| 2015-10-02 | Universes: enforce Set <= i for all Type occurrences. | Matthieu Sozeau |
| 2015-03-11 | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) | Enrico Tassi |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-11-02 | Improving elimination with indices, getting rid of intrusive residual | Hugo Herbelin |
| 2014-11-02 | Supporting "at occs" as a short-hand for "in |- * at occs" in "destruct". | Hugo Herbelin |
| 2014-05-31 | Basic lemmas about the algebraic structure of equality. | Hugo Herbelin |
| 2014-05-07 | Removing comment outdated since eta holds in conversion rule (this | Hugo Herbelin |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2013-08-08 | Side effect free implementation of admit (Isabelle's oracle) | gareuselesinge |
| 2013-05-05 | Improving printing of 'rew' notation | herbelin |
| 2013-04-17 | Added group properties of eq_refl, eq_sym, eq_trans | herbelin |
| 2012-11-15 | Some lemmas on property of rewriting. It will probably be worth at | herbelin |
| 2012-10-24 | Removed a few calls to "Opaque" in Logic.v ineffective since at least | herbelin |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-07-05 | Kills the useless tactic annotations "in |- *" | letouzey |
| 2012-07-05 | Notation: a new annotation "compat 8.x" extending "only parsing" | letouzey |
| 2012-04-12 | "A -> B" is a notation for "forall _ : A, B". | pboutill |
| 2012-04-06 | Fixing a few bugs (see #2571) related to interpretation of multiple binders | herbelin |
| 2012-01-19 | No more use of tauto in Init/ | pboutill |
| 2011-11-21 | theories/, plugins/ and test-suite/ ported to the Arguments vernacular | gareuselesinge |
| 2011-08-10 | Take benefit of bullets available by default in Prelude | herbelin |
| 2011-08-10 | Less ambitious application of a notation for eq_rect. We proposed | herbelin |
