| Age | Commit message (Expand) | Author |
|---|
| 2015-03-13 | CHANGES: more correct equivalent to "constructor tac" syntax. | Arnaud Spiwack |
| 2015-03-11 | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) | Enrico Tassi |
| 2015-02-28 | Explicit in CHANGES incompatibilities introduced in patterns by b2953849 (or ... | Pierre Boutillier |
| 2015-02-24 | CHANGES: Info command + info_auto currently broken. | Arnaud Spiwack |
| 2015-02-15 | Undo: back to 8.4 semantics (Close #3514) | Enrico Tassi |
| 2015-02-15 | Note about "Undo. Undo." in CHANGES | Enrico Tassi |
| 2015-02-15 | Document the behavior change of Instance wrt {|...|}. (Fix for bug #3749) | Guillaume Melquiond |
| 2015-02-13 | Document the issue with trivial inductive types. (Workaround for bug #3984) | Guillaume Melquiond |
| 2015-02-12 | Fix typos about .vio files (thanks Arthur for spotting them) | Enrico Tassi |
| 2015-01-24 | Updating CHANGES (grammar, thanks to AS for pointing it out) + | Hugo Herbelin |
| 2015-01-23 | Typos, grammar, layout in CHANGES (continued). | Hugo Herbelin |
| 2015-01-23 | Typos, grammar, layout in CHANGES. | Hugo Herbelin |
| 2015-01-16 | Documenting the removal of coercions between sig, sigT, sig2, | Hugo Herbelin |
| 2015-01-15 | Move explanations about primitive projections to the manual. | Matthieu Sozeau |
| 2015-01-15 | Update header of CHANGES. | Maxime Dénès |
| 2015-01-15 | Mention guard condition in CHANGES. | Maxime Dénès |
| 2015-01-14 | CHANGES: my recent updates to Ltac. | Arnaud Spiwack |
| 2015-01-13 | More in CHANGES about local definitions | Pierre-Marie Pédrot |
| 2015-01-10 | CHANGES: mention "Optimize (Heap|Proof)" | Enrico Tassi |
| 2015-01-08 | Update + English in CHANGES | Hugo Herbelin |
| 2015-01-08 | Start credits for 8.5. | Matthieu Sozeau |
| 2015-01-08 | Fixed and extend bullet related info/error messages. + doc. | Pierre Courtieu |
| 2015-01-08 | Document native_compute. | Maxime Dénès |
| 2015-01-06 | rename: vi -> vio | Enrico Tassi |
| 2014-12-30 | Document the new behavior of lazymatch. | Guillaume Melquiond |
| 2014-12-30 | more CHANGES | Enrico Tassi |
| 2014-12-23 | Minor modification of CHANGE. | Pierre Courtieu |
| 2014-12-19 | Better doc and a few fixes for Proof using. | Enrico Tassi |
| 2014-12-16 | In CHANGES, alerting about stronger check on notation level modifiers. | Hugo Herbelin |
| 2014-12-15 | About now accepts hypothesis names and goal selector. | Pierre Courtieu |
| 2014-12-12 | Searchxxx now search also the hypothesis and support goal selector. | Pierre Courtieu |
| 2014-11-30 | Documenting the Set Refine Instance Mode. | Pierre-Marie Pédrot |
| 2014-11-18 | Hopefully the last word on having "simpl f" complying with the | Hugo Herbelin |
| 2014-11-18 | Fixing detection of occurrences in the presence of nested subterms for | Hugo Herbelin |
| 2014-11-17 | Documenting use of colors in Coq. | Pierre-Marie Pédrot |
| 2014-11-16 | Enforcing a stronger difference between the two syntaxes "simpl | Hugo Herbelin |
| 2014-11-11 | Updating CHANGES (evars as ident). | Hugo Herbelin |
| 2014-11-11 | American spelling + layout in CHANGES. | Hugo Herbelin |
| 2014-11-04 | Fixing careless name confusion in CHANGES. | Pierre-Marie Pédrot |
| 2014-11-04 | Documenting the change of semantics of the replace tactic. | Pierre-Marie Pédrot |
| 2014-11-02 | Improving elimination with indices, getting rid of intrusive residual | Hugo Herbelin |
| 2014-10-25 | This commit introduces changes in induction and destruct. | Hugo Herbelin |
| 2014-10-24 | Documenting some incompatibilities in (non) Import of ML tactics, | Hugo Herbelin |
| 2014-10-24 | Addressing report #3279 (inconsistency of behavior of the -> and <- | Hugo Herbelin |
| 2014-10-22 | CHANGES: makes explicit the incompatibily introduced by the use of Ltac-defin... | Arnaud Spiwack |
| 2014-10-13 | Mentioning incompatibility shown in #3718 and coming from #3050 | Hugo Herbelin |
| 2014-09-29 | Documenting option -type-in-type. | Hugo Herbelin |
| 2014-09-10 | Fixing inversion after having fixed intros_replacing | Hugo Herbelin |
| 2014-09-09 | Documenting the new Undo semantics | Enrico Tassi |
| 2014-09-08 | Removing the documentation of the XML plugin. | Pierre-Marie Pédrot |
