coq - The formal proof system

Age	Commit message (Expand)	Author
2012-03-30	Typo in a message.	aspiwack
2012-03-20	Fixing alpha-conversion bug #2723 introduced in r12485-12486.	herbelin
2012-03-02	Noise for nothing	pboutill
2012-02-07	A "Grab Existential Variables" to transform the unresolved evars at the end o...	aspiwack
2011-12-19	Fixed some printing details for dependent evars in emacs mode. Patch	courtieu
2011-12-18	Applied patches proposed suggested by Hendrik Tews to fix existential	courtieu
2011-11-23	In emacs mode, prints a list of the dependent existential variables introduced	aspiwack
2011-11-18	Added a printing function to handle single evars	ppedrot
2011-10-25	First attempt at making Print Assumption compatible with opaque modules (fix ...	letouzey
2011-09-12	Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...	aspiwack
2011-08-30	Porting Hendrik's 8.3 patch for proof tree visualization under proof	herbelin
2011-06-10	Revert "Check if recursive calls are guarded before printing "Proof completed"."	pboutill
2011-05-26	Check if recursive calls are guarded before printing "Proof completed".	herbelin
2011-05-24	Made the emacs-U option deprecated. Also removed the old code	courtieu
2011-05-21	Restore display of notation when printing an inductive such as sig	letouzey
2011-05-11	Print Module (Type) M now tries to print more details	letouzey
2011-03-07	Reverted commit r13893 about propagation of more informative	herbelin
2011-03-07	Added propagation of evars unification failure reasons for better	herbelin
2010-12-24	More {raw => glob} changes for consistency	glondu
2010-12-23	Change of nomenclature: rawconstr -> glob_constr	glondu
2010-09-28	Remove some occurrences of "open Termops"	glondu
2010-09-24	Some dead code removal, thanks to Oug analyzer	letouzey
2010-09-02	Improved printing of Unfoldable constants in hints databases (used	herbelin
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-06-12	Fixing spelling: pr_coma -> pr_comma	herbelin
2010-06-06	Added support for Ltac-matching terms with variables bound in the pattern	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2010-04-22	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack
2009-10-28	Integrate a few improvements on typeclasses and Program from the equations br...	msozeau
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-06-11	Simplifying the call to print_no_goals and not calling it when no goal	herbelin
2009-06-06	Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0	herbelin
2009-05-09	- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence	herbelin
2009-03-09	Optionally list opaque constants in addition to axions/variables in	msozeau
2008-12-29	- Added support for subterm matching in SearchAbout.	herbelin
2008-11-26	closed bug 1898: fold x in x; added a reordering primitive tactic	barras
2008-11-09	- Fixed bug 1968 (inversion failing due to a Not_found bug introduced in	herbelin
2008-10-21	duplicated open of Ppconstr	letouzey
2008-08-04	Évolutions diverses et variées.	herbelin
2008-07-17	Uniformisation du format des messages d'erreur (commencent par une	herbelin
2008-07-01	Various bug fixes in type classes and subtac:	msozeau
2008-05-27	Correction du problème de complexité de Print Assumptions :	aspiwack
2008-04-24	- Add pretty-printers for Idpred, Cpred and transparent_state, used for	msozeau
2008-03-10	Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)	herbelin
2007-12-18	Nettoyage de code en vue de la release. Plus de Warning: Unused	aspiwack
2007-12-17	Print Assumptions est pret pour la release.	aspiwack
2007-12-06	Plus de combinateurs sont passés de Util à Option. Le module Options	aspiwack
2007-07-18	Affichage de "thesis" seulement en mode déclaratif	herbelin
2007-06-30	Factorisation des types dans l'affichage des paramètres des (Co)Inductif/Record	herbelin
2007-06-26	killing some more non-exhaustive patterns	letouzey