coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Réorganisation de la structure interne des types de déclarations (decl_kinds)	herbelin	2006-01-28
*	Changement des named_context	gregoire	2005-12-02
*	Types inductifs parametriques	mohring	2005-11-02
*	Standardisation of function names about structures	herbelin	2005-02-18
*	Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed	sacerdot	2005-01-14
*	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
*	Nouvelle en-tête	herbelin	2004-07-16
*	* <style>...</style> tag no longer generated for theory files	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
*	Coqdoc backtrack: HTML special characters are no longer quoted inside # ... #;	sacerdot	2004-04-07
*	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
*	WARNING	sacerdot	2004-04-04
*	LocalFact added as a choice for the "as" attribute of ht:VARIABLE in the	sacerdot	2004-04-01
*	Big bug fixed: interactive local definitions where handled as constants	sacerdot	2004-04-01
*	Output of theory files reimplemented using Buffer.	sacerdot	2004-04-01
*	~keep_sections was now redundant. Got rid of.	sacerdot	2004-04-01
*	En mode batch, recuperation via Declare de l'information si un inductive est ...	herbelin	2004-03-31
*	* WARNING: DTD Change *	sacerdot	2004-03-30
*	declare_internal_constant behaved as declare_constant for proofs (e.g.	sacerdot	2004-03-30
*	No longer used (and probably no longer working) code removed.	sacerdot	2004-03-30
*	Added a <br/> after "Require ...".	sacerdot	2004-03-30
*	Renommage	herbelin	2004-03-30
*	Distinction entre declarations internes (p.ex. _subproof) et declarations uti...	herbelin	2004-03-30
*	Fabrication de l'uri a partir du path utilisateur	herbelin	2004-03-30
*	Retrait debogage	herbelin	2004-03-29
*	Export du type de preuve en cours pour xml	herbelin	2004-03-29
*	Debug prints removed.	sacerdot	2004-03-29
*	Export Require	herbelin	2004-03-29
*	Export des sections; creation COQ_XML_ROOT_LIBRARY si non existant; divers	herbelin	2004-03-27
*	-dead code removed.	sacerdot	2004-03-27
*	Theory file for file A.B.C.v is put in A/B/C.theory.xml.	sacerdot	2004-03-26
*	Ajout exportation des 'theory.xml' + divers	herbelin	2004-03-26
*	ProofTree2Xml is no longer directly used by Xmlcommand.	sacerdot	2004-03-25
*	Dead code removed.	sacerdot	2004-03-25
*	Reparation typo de HH dans MAJ de Claudio	herbelin	2004-03-24
*	MAJ Claudio pour v8	herbelin	2004-03-24
*	la table PARAMETER n'existe plus (mergé dans la table CONSTANT)	letouzey	2002-12-03
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Intégration de la branche mowgli	herbelin	2002-11-05
*	reparation du make depend et du .depend	letouzey	2001-12-19
*	Mise en place d'une méthode directe pour indiquer le type des déclarations ...	herbelin	2001-11-19
*	GROS COMMIT:	barras	2001-11-05
*	Abstraction de l'immplementation de dirpath et implementation dans l'autre se...	herbelin	2001-10-17
*	Déplacement de global_reference dans Names pour pouvoir lier Nametab à gra...	herbelin	2001-10-12