coq - The formal proof system

Age	Commit message (Expand)	Author
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey
2009-01-27	Forgot a file in r11859. Sorry...	puech
2009-01-17	DISCLAIMER	puech
2008-12-29	- Added support for subterm matching in SearchAbout.	herbelin
2008-10-11	Backporting 11445 from 8.2 to trunk (negative conditions in	herbelin
2008-04-23	Prise en compte des coercions dans les clauses "with" même si le type	herbelin
2008-02-22	Merge with lmamane's private branch:	lmamane
2007-12-06	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack
2007-01-10	Merge from Lionel Elie Mamane's private branch:	lmamane
2006-10-28	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin
2006-03-22	Made pretyping a functor over a coercion implementation. Pretyping.Default us...	msozeau
2006-01-11	removes several warnings in contrib/interface	bertot
2006-01-11	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin
2005-12-26	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des G_*...	herbelin
2005-12-26	Achèvement suppression traducteur dans contrib/interface	herbelin
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...	herbelin
2004-11-16	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot
2004-09-17	restructuration des printers: proofs passe avant parsing	barras
2004-02-16	adds a new command for searching a pattern inside the premises of theorems	bertot
2004-02-11	removes a lot comments that may be useful for later code maintenance, but	bertot
2003-11-10	Suppression SearchNamed finalement redondant avec SearchAbout	herbelin
2003-10-23	Conjecture declare maintenant un axiome; reorganisation VernacDefinition	herbelin
2003-10-22	Integration de SearchNamed dans SearchAbout	herbelin
2003-10-13	Ajout d'une fonction de recherche sur les composantes du nom des objets	herbelin
2003-10-10	show_subgoals dans Pfedit	herbelin
2003-04-07	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin
2003-03-12	* empty log message *	barras
2003-01-26	all tactics should be covered now: remains	bertot
2003-01-24	Inspect does not work for pcoq and there is no simple fix because inspect	bertot
2003-01-23	Make sure proof by pointing works.	bertot
2003-01-22	removes all references to ctast.ml the Makefile has been updated accordingly.	bertot
2002-12-12	Ajout du vernac Proof with	gregoire
2002-12-03	la table PARAMETER n'existe plus (mergé dans la table CONSTANT)	letouzey
2002-12-03	Etape intermédiaire d'adaptation de la connexion à pcoq aux nouvelles	bertot
2002-11-14	Réforme de l'interprétation des termes :	herbelin
2002-11-05	Intégration des modifs de la branche mowgli :	herbelin
2002-10-03	Previous version did compile but did not make it possible to actually run	bertot
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-06-05	Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...	herbelin
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin