coq - The formal proof system

Age	Commit message (Expand)	Author
2004-04-04	WARNING	sacerdot
2004-04-02	maj	filliatr
2004-04-01	maj	filliatr
2004-04-01	maj	filliatr
2004-04-01	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-03-31	maj	filliatr
2004-03-31	maj	filliatr
2004-03-31	Morphismes déclarés comme Lemma pas comme Definition	herbelin
2004-03-31	En mode batch, recuperation via Declare de l'information si un inductive est ...	herbelin
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