| Commit message (Expand) | Author | Age |
|---|
| * | 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 |
| * | 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 |
| * | A uniformization step around understand_* and interp_* functions. |  herbelin | 2013-05-09 |
| * | Some documentation of recent changes concerning interfaces |  letouzey | 2012-05-29 |
| * | Moved to a more standard order of arguments (i.e. env followed by evar_map) | herbelin | 2011-10-11 |
| * | Update changelogs |  glondu | 2011-02-11 |
| * | 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 |
| * | Fixed a bug in pretty-printing "induction" and "destruct" due to a | herbelin | 2010-06-13 |
| * | Improved the efficiency of evars traverals thanks to a split of | herbelin | 2010-05-13 |
| * | Removing redundant internal variants of apply tactic and simplification of ML... | herbelin | 2010-04-14 |
| * | Added a function in typing.ml to solve evars of a constr w/o going back down ... | herbelin | 2010-04-05 |
| * | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin | 2009-11-09 |
| * | Restructuration of command.ml + generic infrastructure for inductive schemes | herbelin | 2009-11-08 |
| * | - Cleaning phase of the interfaces of libnames.ml and nametab.ml | herbelin | 2009-08-06 |
| * | - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence | herbelin | 2009-05-09 |
| * | - Cleaning (unification of ML names, removal of obsolete code, | herbelin | 2009-04-27 |
| * | Directory 'contrib' renamed into 'plugins', to end confusion with archive of ... | letouzey | 2009-03-20 |
| * | Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl) | herbelin | 2009-03-17 |
| * | Cleaning/uniformizing the interface of tacticals.mli | herbelin | 2009-03-14 |
| * | - Structuring Numbers and fixing Setoid in stdlib's doc. | herbelin | 2009-01-19 |
| * | - Added support for subterm matching in SearchAbout. | herbelin | 2008-12-29 |
| * | About "apply in": | herbelin | 2008-12-09 |
| * | MAJ diverses | herbelin | 2008-06-11 |
| * | - Patch sur "intros until 0" | herbelin | 2008-06-08 |
| * | - Extension de "generalize" en "generalize c as id at occs". | herbelin | 2008-06-08 |
| * | Mise en place d'un algorithme d'inversion des contraintes de type lors | herbelin | 2008-05-05 |
| * | Correction du bug des types singletons pas sous-type de Set | herbelin | 2008-04-27 |
| * | Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in. | herbelin | 2007-04-28 |
| * | - Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771 | herbelin | 2007-04-18 |
| * | MAJ fichier dev/doc/changes.txt | herbelin | 2006-06-10 |
| * | 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 | 2006-05-23 |
Pierre Letouzey
Hugo Herbelin
herbelin
letouzey
glondu