| 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-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 |
| 2013-05-09 | A uniformization step around understand_* and interp_* functions. | herbelin |
| 2012-05-29 | Some documentation of recent changes concerning interfaces | letouzey |
| 2011-10-11 | Moved to a more standard order of arguments (i.e. env followed by evar_map) | herbelin |
| 2011-02-11 | Update changelogs | 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-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 |
| 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-08-06 | - Cleaning phase of the interfaces of libnames.ml and nametab.ml | 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-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-01-19 | - Structuring Numbers and fixing Setoid in stdlib's doc. | herbelin |
| 2008-12-29 | - Added support for subterm matching in SearchAbout. | herbelin |
| 2008-12-09 | About "apply in": | herbelin |
| 2008-06-11 | MAJ diverses | herbelin |
| 2008-06-08 | - Patch sur "intros until 0" | herbelin |
| 2008-06-08 | - Extension de "generalize" en "generalize c as id at occs". | herbelin |
| 2008-05-05 | Mise en place d'un algorithme d'inversion des contraintes de type lors | herbelin |
| 2008-04-27 | Correction du bug des types singletons pas sous-type de Set | herbelin |
| 2007-04-28 | Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in. | herbelin |
| 2007-04-18 | - Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771 | herbelin |
| 2006-06-10 | MAJ fichier dev/doc/changes.txt | herbelin |
| 2006-05-23 | Mise à jour dev/doc/changes.txt et ajout d'un mot sur TACTIC EXTEND | herbelin |
| 2006-05-23 | Restructuration dossier dev et mise à jour de certaines documentations | herbelin |
