coq - The formal proof system

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