| 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 |