| Age | Commit message (Expand) | Author |
|---|
| 2016-07-18 | Remove the swap tactic from the prelude. | Maxime Dénès |
| 2016-06-18 | Giving a more natural semantics to injection by default. | Hugo Herbelin |
| 2016-06-16 | Adding option "Set Reversible Pattern Implicit" to Specif.v so that an | Hugo Herbelin |
| 2016-04-27 | Revert "Adding option "Set Reversible Pattern Implicit" to Specif.v so that an" | Hugo Herbelin |
| 2016-04-27 | Adding option "Set Reversible Pattern Implicit" to Specif.v so that an | Hugo Herbelin |
| 2016-04-04 | Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into... | Matthieu Sozeau |
| 2016-03-06 | Moving Eauto to a simple ML file. | Pierre-Marie Pédrot |
| 2016-02-23 | Moving tauto.ml4 to a proper ML file. | Pierre-Marie Pédrot |
| 2016-02-22 | Moving the Tauto tactic to proper Ltac. | Pierre-Marie Pédrot |
| 2016-01-21 | Merge branch 'v8.5' | Pierre-Marie Pédrot |
| 2016-01-20 | Update copyright headers. | Maxime Dénès |
| 2015-12-24 | Removing auto from the tactic AST. | Pierre-Marie Pédrot |
| 2015-10-02 | Remove Print Universe directive. | Matthieu Sozeau |
| 2015-10-02 | Universes: enforce Set <= i for all Type occurrences. | Matthieu Sozeau |
| 2015-08-14 | Move type_scope into user space, fix some output logs | Jason Gross |
| 2015-08-14 | Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080 | Jason Gross |
| 2015-08-02 | Reverting 16 last commits, committed mistakenly using the wrong push command. | Hugo Herbelin |
| 2015-08-02 | Adding a notation { x & P } for { x : _ & P }. | Hugo Herbelin |
| 2015-05-09 | Tentatively setting cons and Some with 1st implicit argument maximal | Hugo Herbelin |
| 2015-03-31 | Fix various typos in documentation | Matěj Grabovský |
| 2015-03-11 | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) | Enrico Tassi |
| 2015-02-25 | Reorder the steps of the easy tactic. (Fix for bug #2630) | Guillaume Melquiond |
| 2015-01-15 | Correct restriction of vm_compute when handling universe polymorphic | Matthieu Sozeau |
| 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-10-01 | eta contractions | Pierre Boutillier |
| 2014-09-09 | - Fix printing and parsing of primitive projections, including the Set | Matthieu Sozeau |
| 2014-09-08 | Removing the XML plugin. | Pierre-Marie Pédrot |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross |
| 2014-08-07 | Instead of relying on a trick to make the constructor tactic parse, put | Pierre-Marie Pédrot |
| 2014-08-07 | Removing the "constructor" tactic from the AST. | Pierre-Marie Pédrot |
| 2014-08-05 | Experimentally adding an option for automatically erasing an | Hugo Herbelin |
| 2014-07-09 | Arith: full integration of the "Numbers" modular framework | Pierre Letouzey |
| 2014-05-31 | Basic lemmas about the algebraic structure of equality. | Hugo Herbelin |
| 2014-05-16 | Moving argument-free tactics out of the AST into a dedicated | Pierre-Marie Pédrot |
| 2014-05-12 | Now parsing rules of ML-declared tactics are only made available after the | Pierre-Marie Pédrot |
| 2014-05-07 | Removing comment outdated since eta holds in conversion rule (this | Hugo Herbelin |
| 2014-05-06 | Try a new way of handling template universe levels | Matthieu Sozeau |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-10 | No more Coersion in Init. | Pierre Boutillier |
| 2014-04-10 | Define [projT3] and [proj3_sig] | Jason Gross |
| 2014-01-24 | [Coercion]s use [Sortclass], not [Prop] (in docs) | Jason Gross |
| 2013-12-12 | Better unification for [projT1] and [proj1_sig]. | Jason Gross |
| 2013-11-20 | Adding Acc_intro_generator in order to help computations of Function in parti... | forest |
| 2013-08-08 | Side effect free implementation of admit (Isabelle's oracle) | gareuselesinge |
| 2013-05-05 | Improving printing of 'rew' notation | herbelin |
| 2013-05-05 | Relaxing the constraint on eta-expanding on the fly while looking for | herbelin |
| 2013-04-17 | Added group properties of eq_refl, eq_sym, eq_trans | herbelin |
