| Commit message (Expand) | Author | Age |
* | [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-25 |
* | Makefile: compat5* moved in grammar/, less -I given to camlp4o | Pierre Letouzey | 2016-06-21 |
* | Documenting API changes in dev/doc/changes.txt. | Pierre-Marie Pédrot | 2016-06-09 |
* | Merge PR #197. | Pierre-Marie Pédrot | 2016-06-09 |
|\ |
|
* | | 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-08 |
* | A slight phase of documentation and uniformization of names of | Hugo Herbelin | 2016-06-02 |
* | 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-06-01 |
* | | Feedback cleanup | Emilio Jesus Gallego Arias | 2016-05-31 |
|/ |
|
* | A note concerning the "Drop" command. | Matej Kosik | 2016-05-03 |
* | setup.txt : a guide explaining taming Emacs, Merlin, Company, Ocamldebug. | Matej Kosik | 2016-05-03 |
* | Creating a dedicated ltac/ folder for Hightactics. | Pierre-Marie Pédrot | 2016-03-21 |
* | Documenting changes. | Pierre-Marie Pédrot | 2016-03-20 |
* | Documenting the change of EXTEND macros. | Pierre-Marie Pédrot | 2016-03-18 |
* | Merge branch 'render-prehistory' of https://github.com/aspiwack/coq into aspi... | Hugo Herbelin | 2016-03-09 |
|\ |
|
* | | CLEANUP: Context.{Rel,Named}.Declaration.t | Matej Kosik | 2016-02-09 |
* | | CLEANUP: kernel/context.ml{,i} | Matej Kosik | 2016-01-11 |
* | | Update history of revisions. | Hugo Herbelin | 2015-12-02 |
* | | Being more precise and faithful about the origin of the file reporting | Hugo Herbelin | 2015-11-16 |
| * | 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-11-11 |
|/ |
|
* | Fix some typos. | Guillaume Melquiond | 2015-10-13 |
* | Minor typo in universe polymorphism doc. | Maxime Dénès | 2015-10-09 |
* | 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 | 2015-10-02 |
* | Switch the few remaining iso-latin-1 files to utf8 | Pierre Letouzey | 2014-12-09 |
* | Uniformisation of the order of arguments env and sigma. | Hugo Herbelin | 2014-09-12 |
* | A reorganization of the "assert" tactics (hopefully uniform naming | Hugo Herbelin | 2014-08-18 |
* | Reorganisation of intropattern code | Hugo Herbelin | 2014-08-18 |
* | A tentative uniform naming policy in module Inductiveops. | Hugo Herbelin | 2014-08-01 |
* | Moved code for finding subterms (pattern, induction, set, generalize, ...) | Hugo Herbelin | 2014-06-28 |
* | Change Ltac constr matching semantics to consider universes when merging two | Matthieu Sozeau | 2014-06-15 |
* | A little bit of documentation about V5.10 and V6.3 and V7. | Hugo Herbelin | 2014-06-01 |
* | 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-08 |
* | 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 | 2014-05-06 |
* | Set officially the minimal OCaml requirement to 3.12.1 | Pierre Letouzey | 2014-03-02 |
* | Makefile: re-introduce 2 phases to avoid make strange -include's | Pierre Letouzey | 2014-02-27 |
* | A file listing old svn branches and tags | letouzey | 2013-11-18 |
* | A uniformization step around understand_* and interp_* functions. | herbelin | 2013-05-09 |
* | Revert "remove -rectypes except for term.ml" | mdenes | 2013-01-22 |
* | remove -rectypes except for term.ml | letouzey | 2012-10-06 |