coq - The formal proof system

Age	Commit message (Expand)	Author
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	A few changes backtracked:	sacerdot
2004-04-06	maj	filliatr
2004-04-06	1. In -html mode the generated files are well-formed XML files	sacerdot
2004-04-06	Fake dependent products in inductive definition types are no longer replaced	sacerdot
2004-04-06	Premier jet annonce finale	herbelin
2004-04-06	Important bug fix: since coqdoc is now quoting XML reserved characters in	sacerdot
2004-04-06	MAJ V8.0 finale	herbelin
2004-04-06	sumbool et sumor affich avec 'if' si possible	herbelin
2004-04-06	warning dialog when save fails	marche
2004-04-06	Bug sur commit 1.44 dans find_constructor (Not_Found pas rattrape)	herbelin
2004-04-06	echappement de <, > et & en HTML	filliatr
2004-04-05	maj	filliatr
2004-04-05	Déclaration des record au chargement (ce n'est pas une question de visibilit...	herbelin
2004-04-05	Since coqdoc produces (X)HTML, HTML character entities can be used	sacerdot
2004-04-05	correction rapide du bug PR\#592	letouzey
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