| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2014-09-08 | CHANGES: existential variables are always "substituted" in the new tactic eng... | Arnaud Spiwack |
| 2014-09-08 | CHANGES: Ltac's [refine] accepts [uconstr]. | Arnaud Spiwack |
| 2014-09-08 | CHANGES: [revgoals]. | Arnaud Spiwack |
| 2014-09-08 | CHANGES: [Variant], [Set Nonrecursive Elimination Schemes]. | Arnaud Spiwack |
| 2014-09-08 | CHANGES: binder names from Ltac identifiers. | Arnaud Spiwack |
| 2014-08-25 | "allows to", like "allowing to", is improper | Jason Gross |
| 2014-08-25 | Grammar: "allowing to" is not proper English | Jason Gross |
| 2014-08-18 | Adding a new intro-pattern for "apply in" on the fly. Using syntax | Hugo Herbelin |
| 2014-08-05 | Uncountably many bullets (+,-,*,++,--,**,+++,...). | Hugo Herbelin |
| 2014-08-05 | Experimentally adding an option for automatically erasing an | Hugo Herbelin |
| 2014-08-05 | Adding a syntax "enough" for the variant of "assert" with the order of | Hugo Herbelin |
| 2014-08-05 | A new step in the new "standard" naming policy for propositional hypotheses | Hugo Herbelin |
| 2014-08-01 | CHANGES: [>…]. | Arnaud Spiwack |
| 2014-08-01 | CHANGES: [numgoals] and [guard]. | Arnaud Spiwack |
| 2014-07-31 | Making the error message about bullets more precise. | Pierre Courtieu |
| 2014-07-29 | CHANGES: untyped terms in tactics | Arnaud Spiwack |
| 2014-07-25 | CHANGES: cycle and swap. | Arnaud Spiwack |
| 2014-07-25 | CHANGES: yellow in Coqide. | Arnaud Spiwack |
| 2014-07-25 | CHANGE: add Derive. | Arnaud Spiwack |
| 2014-07-25 | CHANGE: document the features of the new tactic engine. | Arnaud Spiwack |
| 2014-07-21 | Documenting the changes of Locate semantics. | Pierre-Marie Pédrot |
| 2014-07-21 | Documenting the need of the "DECLARE PLUGIN" statement. | Pierre-Marie Pédrot |
| 2014-07-21 | Documenting the change of semantics of the "constructor" tactic. | Pierre-Marie Pédrot |
| 2014-07-13 | Mentioning the incompatibility due to fixing bug #2996 (see #3418). | Hugo Herbelin |
