| Commit message (Expand) | Author | Age |
|---|
| * | 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 |
| * | Remove broken makefile option NO_RECOMPILE_LIB | letouzey | 2012-09-20 |
| * | Some documentation of recent changes concerning interfaces | letouzey | 2012-05-29 |
| * | debugging.txt: no more typing of #use "include" if using .ocamlinit | letouzey | 2011-10-15 |
| * | Moved to a more standard order of arguments (i.e. env followed by evar_map) | herbelin | 2011-10-11 |
| * | Moving never-used comments from Zhints.v to dev/doc so as not to | herbelin | 2011-10-01 |
| * | A few comments and a dev file to summarize issues with unification | herbelin | 2011-06-13 |
| * | Update changelogs |  glondu | 2011-02-11 |
| * | Remove obsolete script univdot, update dev doc about universes | glondu | 2010-12-24 |
| * | Simplify tactic(_)-bound arguments in TACTIC EXTEND rules | glondu | 2010-09-30 |
| * | Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt). | herbelin | 2010-07-22 |
| * | Made tclABSTRACT normalize evars before saying it does not support | herbelin | 2010-06-29 |
| * | Fixed commit 13125 (stricter check of induction args): an interpretation | herbelin | 2010-06-14 |
Matej Kosik
Pierre-Marie Pédrot
Hugo Herbelin
Arnaud Spiwack
Guillaume Melquiond
Maxime Dénès
Matthieu Sozeau
Pierre Letouzey
Matthieu Sozeau
letouzey
herbelin
mdenes
glondu