aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/doc/changes.txt
Commit message (Expand)AuthorAge
* Some documentation of recent changes concerning interfacesGravatar letouzey2012-05-29
* Moved to a more standard order of arguments (i.e. env followed by evar_map)Gravatar herbelin2011-10-11
* Update changelogsGravatar glondu2011-02-11
* Simplify tactic(_)-bound arguments in TACTIC EXTEND rulesGravatar glondu2010-09-30
* Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).Gravatar herbelin2010-07-22
* Made tclABSTRACT normalize evars before saying it does not supportGravatar herbelin2010-06-29
* Fixed commit 13125 (stricter check of induction args): an interpretationGravatar herbelin2010-06-14
* Fixed a bug in pretty-printing "induction" and "destruct" due to aGravatar herbelin2010-06-13
* Improved the efficiency of evars traverals thanks to a split ofGravatar herbelin2010-05-13
* Removing redundant internal variants of apply tactic and simplification of ML...Gravatar herbelin2010-04-14
* Added a function in typing.ml to solve evars of a constr w/o going back down ...Gravatar herbelin2010-04-05
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
* - Cleaning (unification of ML names, removal of obsolete code,Gravatar herbelin2009-04-27
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20
* Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)Gravatar herbelin2009-03-17
* Cleaning/uniformizing the interface of tacticals.mliGravatar herbelin2009-03-14
* - Structuring Numbers and fixing Setoid in stdlib's doc.Gravatar herbelin2009-01-19
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* About "apply in":Gravatar herbelin2008-12-09
* MAJ diversesGravatar herbelin2008-06-11
* - Patch sur "intros until 0"Gravatar herbelin2008-06-08
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* Mise en place d'un algorithme d'inversion des contraintes de type lorsGravatar herbelin2008-05-05
* Correction du bug des types singletons pas sous-type de SetGravatar herbelin2008-04-27
* Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.Gravatar herbelin2007-04-28
* - Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771Gravatar herbelin2007-04-18
* MAJ fichier dev/doc/changes.txtGravatar herbelin2006-06-10
* Mise à jour dev/doc/changes.txt et ajout d'un mot sur TACTIC EXTENDGravatar herbelin2006-05-23
* Restructuration dossier dev et mise à jour de certaines documentationsGravatar herbelin2006-05-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 06:56:00 +0000