coq - The formal proof system

Age	Commit message (Expand)	Author
2020-08-25	Modify Init/Wf.v to compile with -mangle-names	Jasper Hugunin
2020-04-21	Moving the main Require Export Ltac in Prelude.v.	Hugo Herbelin
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-03-06	Fix #11738 : Funind using deprecated Coqlib API.	Pierre Courtieu
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2018-10-10	[coqlib] Rebindable Coqlib namespace.	Emilio Jesus Gallego Arias
2018-02-27	Update headers following #6543.	Théo Zimmermann
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2016-07-18	Replacing deprecated Implicit Arguments in prelude.	Maxime Dénès
2016-01-20	Update copyright headers.	Maxime Dénès
2015-01-12	Update headers.	Maxime Dénès
2014-08-05	Experimentally adding an option for automatically erasing an	Hugo Herbelin
2013-11-20	Adding Acc_intro_generator in order to help computations of Function in parti...	forest
2012-08-08	Updating headers.	herbelin
2012-07-05	Kills the useless tactic annotations "in \|- *"	letouzey
2010-10-03	Using multiple lists of implicit arguments in Program for preserving	herbelin
2010-07-24	Updated all headers for 8.3 and trunk	herbelin
2010-04-29	Remove the svn-specific $Id$ annotations	letouzey
2009-11-02	Remove various useless {struct} annotations	letouzey
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2008-07-23	Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized the	herbelin
2008-03-23	Nettoyage Wf.v et unification (suite remarques faites sur cocorico)	herbelin
2008-03-15	Do a second pass on the treatment of user-given implicit arguments. Now	msozeau
2008-03-04	still one more substituion s/Set/Type/	letouzey
2008-02-26	Proper implicit arguments handling for assumptions	msozeau
2006-06-25	repetition d'hypotheses dans well_founded_induction_type_2	letouzey
2006-03-17	Modification des propriétés (svn:executable)	notin
2006-02-06	Application des remarques de Pierre Casteran (A:Type plutôt que A:Set) et Ru...	herbelin
2006-01-22	Application de la suggestion de Nicolas Magaud (#1060)	herbelin
2006-01-21	Backtrack commit précédent: la préservation de l'énoncé exact Acc_ind es...	herbelin
2006-01-21	Préservation énoncé exact Acc_ind par choix nom 'a' comme paramètre de Acc	herbelin
2005-11-30	changement parametres inductifs dans les theories	mohring
2005-05-19	Documentation	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2003-11-29	Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states ...	herbelin
2003-09-28	well_founded_induction de nouveau transparent	letouzey
2003-09-23	Fusion des fichiers de syntaxe de Init avec les fichiers de définition; Type...	herbelin
2003-07-08	recursion bien fondee sur des pairs	filliatr
2003-05-21	Concentration des notations officielles dans Init/Notations; restructuration ...	herbelin
2003-04-28	Un principe light d'elimination de Acc, suivant les remarques de Yves Bertot	letouzey
2003-04-09	Activation des implicites pour la v8	herbelin
2003-03-12	* empty log message *	barras
2002-04-17	Uniformisation (Qed/Save et Implicits Arguments)	herbelin
2002-02-19	Uniformisation des theoremes dans Set et Type (def. de Acc_rect et	barras
2002-02-14	option -dump-glob pour coqdoc	filliatr
2002-01-09	MAJ des Id pour coqweb	herbelin
2001-11-14	Suppression d'Export redondants	herbelin
2001-08-05	Expérimentation de NewDestruct et parfois NewInduction	herbelin
2001-04-11	documentation automatique de la bibliothèque standard	filliatr
2001-03-15	entetes	filliatr