| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2014-03-02 | Set officially the minimal OCaml requirement to 3.12.1 | Pierre Letouzey |
| 2014-02-27 | Makefile: re-introduce 2 phases to avoid make strange -include's | Pierre Letouzey |
| 2013-11-18 | A file listing old svn branches and tags | letouzey |
| 2013-05-09 | A uniformization step around understand_* and interp_* functions. | herbelin |
| 2013-01-22 | Revert "remove -rectypes except for term.ml" | mdenes |
| 2012-10-06 | remove -rectypes except for term.ml | letouzey |
| 2012-09-20 | Remove broken makefile option NO_RECOMPILE_LIB | letouzey |
| 2012-05-29 | Some documentation of recent changes concerning interfaces | letouzey |
| 2011-10-15 | debugging.txt: no more typing of #use "include" if using .ocamlinit | letouzey |
| 2011-10-11 | Moved to a more standard order of arguments (i.e. env followed by evar_map) | herbelin |
| 2011-10-01 | Moving never-used comments from Zhints.v to dev/doc so as not to | herbelin |
| 2011-06-13 | A few comments and a dev file to summarize issues with unification | herbelin |
| 2011-02-11 | Update changelogs | glondu |
| 2010-12-24 | Remove obsolete script univdot, update dev doc about universes | glondu |
| 2010-09-30 | Simplify tactic(_)-bound arguments in TACTIC EXTEND rules | glondu |
| 2010-07-22 | Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt). | herbelin |
| 2010-06-29 | Made tclABSTRACT normalize evars before saying it does not support | herbelin |
| 2010-06-14 | Fixed commit 13125 (stricter check of induction args): an interpretation | herbelin |
| 2010-06-13 | Fixed a bug in pretty-printing "induction" and "destruct" due to a | herbelin |
| 2010-06-09 | Backported r13080 (support for open terms in ltac matching) from trunk to v8.3. | herbelin |
| 2010-06-06 | Updated performance analysis file | herbelin |
| 2010-05-13 | Improved the efficiency of evars traverals thanks to a split of | herbelin |
| 2010-04-14 | Removing redundant internal variants of apply tactic and simplification of ML... | herbelin |
| 2010-04-05 | Added a function in typing.ml to solve evars of a constr w/o going back down ... | herbelin |
| 2010-03-04 | Makefile: cleanup of comments + a few words about recent changes in dev/doc/b... | letouzey |
| 2010-01-04 | Few misc. updates. | herbelin |
| 2009-12-13 | Addition of mergesort + cleaning of the Sorting library | herbelin |
| 2009-11-09 | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin |
| 2009-11-08 | Restructuration of command.ml + generic infrastructure for inductive schemes | herbelin |
| 2009-10-08 | Fixed clash names in Relations (see bug report #2152) and make names | herbelin |
| 2009-08-14 | Mise à jour du document de révision de la stdlib et déplacement de la | herbelin |
| 2009-08-06 | - Cleaning phase of the interfaces of libnames.ml and nametab.ml | herbelin |
| 2009-05-24 | Moved and completed the history of Coq versions from the | herbelin |
| 2009-05-09 | - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence | herbelin |
| 2009-04-27 | - Cleaning (unification of ML names, removal of obsolete code, | herbelin |
| 2009-04-14 | Correction du patch -rectypes pour ocaml 3.10 | vsiles |
| 2009-03-20 | Directory 'contrib' renamed into 'plugins', to end confusion with archive of ... | letouzey |
| 2009-03-17 | Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl) | herbelin |
| 2009-03-14 | Cleaning/uniformizing the interface of tacticals.mli | herbelin |
| 2009-02-17 | #rectypes was already automatically added when using 3.11 | herbelin |
| 2009-02-17 | Made hack to have Drop and #use"include" working with ocaml 3.10 public | herbelin |
| 2009-02-11 | Document how FIND_VCS_CLAUSE has to be used | lmamane |
