| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2014-04-09 | Revert "Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with... | Pierre Boutillier |
| 2014-04-08 | Add an option -Q (tentative name). | Guillaume Melquiond |
| 2014-04-07 | Revert part of eba6b75 as coq_makefile ignores -I if it overlaps with -R. (Fi... | Guillaume Melquiond |
| 2014-04-06 | Change handling of loadpath and mlpath. | Guillaume Melquiond |
| 2014-01-30 | Coqmktop without Sys.command, changes in ./configure -*byteflags options | Pierre Letouzey |
| 2014-01-25 | More in CHANGES. | Pierre-Marie Pédrot |
| 2014-01-10 | Omega: avoiding distinct proof-terms on repeated identical runs | Pierre Letouzey |
| 2013-12-11 | Documenting the tactic-in-term construction. | Pierre-Marie Pédrot |
| 2013-08-22 | Change in vo format : digest aren't Marshalled anymore | letouzey |
| 2013-07-09 | Revising r16550 about providing intro patterns for applying injection: | herbelin |
| 2013-06-06 | Document changes and add missing documentation for Program options. | msozeau |
| 2013-06-02 | Making the behavior of "injection ... as ..." more natural: | herbelin |
| 2013-06-02 | Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as an | herbelin |
| 2013-05-29 | Documenting the "appcontext" by default. | ppedrot |
| 2013-05-14 | "change ... in ..." and "simpl ... in ..." now consider nested | herbelin |
| 2013-05-05 | Reporting the change on matching partial applications in patterns of | herbelin |
| 2013-04-17 | Renaming SearchAbout into Search and Search into SearchHead. | herbelin |
| 2013-03-21 | Using hnf instead of "intro H" for forcing reduction to a product. | herbelin |
| 2013-03-21 | Fixing an old pecularity of "red": head betaiota redexes are now | herbelin |
| 2013-03-11 | Allowing (Co)Fixpoint to be defined local and Let-style. | ppedrot |
