coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Export de l'information si un inductive est un record ou non (pour xml)	herbelin	2004-03-31
*	Fake dependent types in constructors of inductive types are now preserved.	sacerdot	2004-03-31
*	maj	filliatr	2004-03-30
*	* WARNING: DTD Change *	sacerdot	2004-03-30
*	The XML exportation hook for require is now active for:	sacerdot	2004-03-30
*	declare_internal_constant behaved as declare_constant for proofs (e.g.	sacerdot	2004-03-30
*	Heuristique pour traduire if-then-else quand le re-typage echoue	herbelin	2004-03-30
*	Distinction entre declarations internes (p.ex. _subproof) et declarations uti...	herbelin	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
*	syntax error: dandling in	sacerdot	2004-03-30
*	Renommage	herbelin	2004-03-30
*	2 choix incorrects	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
*	maj	filliatr	2004-03-29
*	maj	filliatr	2004-03-29
*	Retrait debogage	herbelin	2004-03-29
*	Export du type de preuve en cours pour xml	herbelin	2004-03-29
*	tools/coq_vo2xml removed since no longer in use.	sacerdot	2004-03-29
*	"xml" target removed from generated makefiles (since it was no longer used)	sacerdot	2004-03-29
*	MAJ	kirchner	2004-03-29
*	Debug prints removed.	sacerdot	2004-03-29
*	Export Require	herbelin	2004-03-29
*	Crocret xml pour Require	herbelin	2004-03-29
*	Commentaires	herbelin	2004-03-29
*	Typo	herbelin	2004-03-29
*	maj	filliatr	2004-03-28
*	maj	filliatr	2004-03-28
*	Nom qualifié pour option -top	herbelin	2004-03-28
*	Désaffectation de l'usage de Top dans Names (maintenant contrôlé dans coqt...	herbelin	2004-03-28
*	MAJ	herbelin	2004-03-28
*	Ajout option -top pour changer le nom 'Top' du toplevel	herbelin	2004-03-28
*	Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ...	herbelin	2004-03-28
*	Crochets pour exported les sections en xml	herbelin	2004-03-27
*	Export des sections; creation COQ_XML_ROOT_LIBRARY si non existant; divers	herbelin	2004-03-27
*	Gestion maintenant purement fonctionnelle des implicites des point-fixes; ajo...	herbelin	2004-03-27
*	Export compute_arguments_scope pour utilisation local a la construction des i...	herbelin	2004-03-27
*	-dead code removed.	sacerdot	2004-03-27
*	maj	filliatr	2004-03-27
*	maj	filliatr	2004-03-27
*	Theory file for file A.B.C.v is put in A/B/C.theory.xml.	sacerdot	2004-03-26
*	Ajout option raw-comments pour supprimer affichage de <table>	herbelin	2004-03-26
*	Ajout option raw-comments pour supprimer affichage de <table>; typos	herbelin	2004-03-26
*	MAJ mot-cles	herbelin	2004-03-26
*	Bug <BR>; ajout option raw_comment pas d'affichage de <table>; MAJ mot-cles	herbelin	2004-03-26
*	Ajout exportation des 'theory.xml' + divers	herbelin	2004-03-26
*	Ajout entree pour exporter les debuts et fins de compilation en mode -xml	herbelin	2004-03-26
*	Ajout entree pour exporter les commentaires en mode -xml	herbelin	2004-03-26
*	Memorisation du type de variable (Hyp or Var)	herbelin	2004-03-26