coq - The formal proof system

Age	Commit message (Expand)	Author
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