| Age | Commit message (Expand) | Author |
|---|
| 2016-08-16 | Merge PR #237 into v8.6 | Pierre-Marie Pédrot |
| 2016-07-05 | FIX: "dev/doc/changes.txt" | Matej Kosik |
| 2016-07-04 | Add a renaming of Tacexpr.TacDynamic | Jason Gross |
| 2016-07-03 | Mention recent renaming of files in dev/doc/changes.txt. | Maxime Dénès |
| 2016-07-01 | Add and document match, fix and cofix reduction flags. | Maxime Dénès |
| 2016-07-01 | Separate flags for fix/cofix/match reduction and clean reduction function names. | Maxime Dénès |
| 2016-06-25 | [doc] Update changes for feedback. | Emilio Jesus Gallego Arias |
| 2016-06-25 | [feedback] Add optional ?loc parameter to loggers. | Emilio Jesus Gallego Arias |
| 2016-06-21 | Makefile: compat5* moved in grammar/, less -I given to camlp4o | Pierre Letouzey |
| 2016-06-09 | Documenting API changes in dev/doc/changes.txt. | Pierre-Marie Pédrot |
| 2016-06-09 | Merge PR #197. | Pierre-Marie Pédrot |
| 2016-06-08 | Adding profiling developer information in dev/doc/profiling.txt. | Pierre-Marie Pédrot |
| 2016-06-08 | Add an explicit replacement rule for Refine module | Jason Gross |
| 2016-06-08 | Officially discontinue the experimental coq build via ocamlbuild | Pierre Letouzey |
| 2016-06-02 | A slight phase of documentation and uniformization of names of | Hugo Herbelin |
| 2016-06-01 | Merge branch 'yet-another-makefile-bigbang' into trunk | Pierre Letouzey |
| 2016-06-01 | Yet another Makefile reform : a unique phase without nasty make tricks | Pierre Letouzey |
| 2016-05-31 | Feedback cleanup | Emilio Jesus Gallego Arias |
| 2016-05-03 | A note concerning the "Drop" command. | Matej Kosik |
| 2016-05-03 | setup.txt : a guide explaining taming Emacs, Merlin, Company, Ocamldebug. | Matej Kosik |
| 2016-03-21 | Creating a dedicated ltac/ folder for Hightactics. | Pierre-Marie Pédrot |
| 2016-03-20 | Documenting changes. | Pierre-Marie Pédrot |
| 2016-03-18 | Documenting the change of EXTEND macros. | Pierre-Marie Pédrot |
| 2016-03-09 | Merge branch 'render-prehistory' of https://github.com/aspiwack/coq into aspi... | Hugo Herbelin |
| 2016-02-09 | CLEANUP: Context.{Rel,Named}.Declaration.t | Matej Kosik |
| 2016-01-11 | CLEANUP: kernel/context.ml{,i} | Matej Kosik |
| 2015-12-02 | Update history of revisions. | Hugo Herbelin |
| 2015-11-16 | Being more precise and faithful about the origin of the file reporting | Hugo Herbelin |
| 2015-11-11 | Prehistory of Coq: move the bibliographic references to a dedicated section. | Arnaud Spiwack |
| 2015-11-11 | Prehistory of Coq: justification of the plain text. | Arnaud Spiwack |
| 2015-11-11 | Prehistory of Coq: consistency. | Arnaud Spiwack |
| 2015-11-11 | Prehistory of Coq: various corrections on English. | Arnaud Spiwack |
| 2015-11-11 | Prehistory of Coq: asciidoc conversion. | Arnaud Spiwack |
| 2015-10-13 | Fix some typos. | Guillaume Melquiond |
| 2015-10-09 | Minor typo in universe polymorphism doc. | Maxime Dénès |
| 2015-10-02 | Updating versions history with data from Gérard. | Hugo Herbelin |
| 2015-10-02 | Update the history of versions with recent versions. | Hugo Herbelin |
| 2015-10-02 | Univs: More info for developers. | Matthieu Sozeau |
| 2014-12-09 | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey |
| 2014-09-12 | Uniformisation of the order of arguments env and sigma. | Hugo Herbelin |
| 2014-08-18 | A reorganization of the "assert" tactics (hopefully uniform naming | Hugo Herbelin |
| 2014-08-18 | Reorganisation of intropattern code | Hugo Herbelin |
| 2014-08-01 | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin |
| 2014-06-28 | Moved code for finding subterms (pattern, induction, set, generalize, ...) | Hugo Herbelin |
| 2014-06-15 | Change Ltac constr matching semantics to consider universes when merging two | Matthieu Sozeau |
| 2014-06-01 | A little bit of documentation about V5.10 and V6.3 and V7. | Hugo Herbelin |
| 2014-05-08 | Isolating a function "make_abstraction", new name of "letin_abstract", | Hugo Herbelin |
| 2014-05-08 | Renaming new_induct -> induction; new_destruct -> destruct. | Hugo Herbelin |
| 2014-05-06 | Add incompatibilities paragraph in doc about universe polymorphism. | Matthieu Sozeau |
| 2014-05-06 | Add doc on the new API for universe polymorphism and primitive projections | Matthieu Sozeau |
