coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Changement des named_context	gregoire	2005-12-02
*	pas besoin de List.length pour savoir si une liste est vide	letouzey	2005-08-19
*	Adoption du nom canonique global_of_constr pour éviter confusion avec type r...	herbelin	2005-05-20
*	Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed	sacerdot	2005-01-14
*	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot	2004-11-16
*	hiding the meta_map in evar_defs	barras	2004-09-15
*	The innersort is now computed as the more precise sort between the	sacerdot	2004-09-08
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	Nouvelle en-tête	herbelin	2004-07-16
*	- recent changes to doubleTypeInference.ml (that introduced double	sacerdot	2004-07-08
*	Commit to perform double type inference also on inner types.	sacerdot	2004-07-08
*	Licence changed from GPL to Lesser GPL.	sacerdot	2004-06-26
*	Copyright notice of files in contrib/xml made uniform.	sacerdot	2004-04-07
*	CoRN CProp detection improved: products of "sort" CProp are now recognized	sacerdot	2004-04-07
*	Fake dependent products in inductive definition types are no longer replaced	sacerdot	2004-04-06
*	~keep_sections was now redundant. Got rid of.	sacerdot	2004-04-01
*	Fake dependent types in constructors of inductive types are now preserved.	sacerdot	2004-03-31
*	syntax error: dandling in	sacerdot	2004-03-30
*	2 choix incorrects	herbelin	2004-03-30
*	Fabrication de l'uri a partir du path utilisateur	herbelin	2004-03-30
*	Fix and Cofix blocks with mutually defined functions having the same	sacerdot	2004-03-25
*	Comment removed.	sacerdot	2004-03-25
*	MAJ Claudio pour v8	herbelin	2004-03-24
*	* empty log message *	barras	2003-03-12
*	Petit netoyage dans lib	coq	2002-12-19
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Intégration de la branche mowgli	herbelin	2002-11-05