coq - The formal proof system

Age	Commit message (Expand)	Author
2004-03-31	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-30	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-29	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-28	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-27	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-26	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