coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	affichage des ... dans les scripts	barras	2006-10-16
*	Détection ocaml 3.09 des variables non utilisées (trop peu pour solliciter ...	herbelin	2006-10-03
*	Declarative Proof Language: main commit	corbinea	2006-09-20
*	Correction bug #1192	notin	2006-07-18
*	Correction bug 1172 + correction en passant de la taille des paramètres de f...	herbelin	2006-07-07
*	Clarification role de library_part : renommage en remove_section_part	herbelin	2006-05-23
*	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin	2006-05-23
*	Standardisation du nom des méthodes de Evd	herbelin	2006-04-28
*	Message d'erreur plus informatif	herbelin	2006-04-27
*	- Documentation of the Program tactics.	msozeau	2006-04-07
*	Correction bug #842 (rename d'une hyp du contexte)	herbelin	2006-03-01
*	Réorganisation de la structure interne des types de déclarations (decl_kinds)	herbelin	2006-01-28
*	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin	2006-01-11
*	Renommage des Ppnew en Pp (et déplacement dans parsing); renommage des G_*...	herbelin	2005-12-26
*	Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...	herbelin	2005-12-26
*	Changement des named_context	gregoire	2005-12-02
*	Types inductifs parametriques	mohring	2005-11-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
*	Unsharing before exportation to ensure uniqueness of xml id's	herbelin	2005-03-15
*	Standardisation of function names about structures	herbelin	2005-02-18
*	Ajout printer direct cic vers xml	herbelin	2005-02-04
*	Export du printer xml vers tacinterp	herbelin	2005-02-04
*	Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed	sacerdot	2005-01-14
*	Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...	herbelin	2005-01-02
*	Orthographe!	herbelin	2004-12-03
*	IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).	sacerdot	2004-11-16
*	Suppression IsConjecture redondant avec Conjectural	herbelin	2004-10-11
*	restructuration des printers: proofs passe avant parsing	barras	2004-09-17
*	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
*	The code used to compare the synthesized and the expected type (if available)	sacerdot	2004-09-08
*	deuxieme vague de modifs: evar_defs fonctionnel	barras	2004-09-07
*	premiere reorganisation de l\'unification	barras	2004-09-03
*	Nouvelle en-tête	herbelin	2004-07-16
*	* <style>...</style> tag no longer generated for theory files	sacerdot	2004-07-08
*	- 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
*	Constants just after a "Let id : t. ... Qed" local variable declaration were	sacerdot	2004-07-05
*	updated printing of evar context (may loop ?)	corbinea	2004-06-30
*	Licence changed from GPL to Lesser GPL.	sacerdot	2004-06-26
*	Copyright notice of files in contrib/xml made uniform.	sacerdot	2004-04-07
*	Old file. The new version of this script is no longer distributed with	sacerdot	2004-04-07
*	- theoryobject.dtd is the DTD for .theory files	sacerdot	2004-04-07
*	Loic code to pretty-print the generated proof-tree debranched (since it	sacerdot	2004-04-07
*	CoRN CProp detection improved: products of "sort" CProp are now recognized	sacerdot	2004-04-07
*	Coqdoc backtrack: HTML special characters are no longer quoted inside # ... #;	sacerdot	2004-04-07
*	Fake dependent products in inductive definition types are no longer replaced	sacerdot	2004-04-06
*	Important bug fix: since coqdoc is now quoting XML reserved characters in	sacerdot	2004-04-06
*	Since coqdoc produces (X)HTML, HTML character entities can be used	sacerdot	2004-04-05