| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2014-07-13 | Adding a "time" tactical for benchmarking purposes. In case the tactic | Hugo Herbelin |
| 2014-06-30 | Synchronized names from the "as" clause with the skeleton of the | Hugo Herbelin |
| 2014-06-28 | Updating CHANGES w.r.t. opacity in type inference + layout of file. | Hugo Herbelin |
| 2014-06-23 | Add some compatibility notes on the changes to [change] and unification in ge... | Matthieu Sozeau |
| 2014-06-01 | Use of "H"-based names for propositional hypotheses obtained by | Hugo Herbelin |
| 2014-05-31 | More on injection over a projectable "existT". - Fixing syntax "injection ...... | Hugo Herbelin |
| 2014-05-18 | Restored old behavior of injection on proofs by default. | Maxime Dénès |
| 2014-05-09 | More documentation of new features in CHANGE. | Pierre-Marie Pédrot |
| 2014-05-08 | Simplification and improvement of "subst x" in such a way that it | Hugo Herbelin |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-30 | Document changes on injection. | Maxime Dénès |
