coq - The formal proof system

Age	Commit message (Expand)	Author
2007-11-01	In agreement with Laurent Thery, start migration of auxiliary results	letouzey
2007-10-25	Adding BigQ and proofs	thery
2007-10-04	Added the proof (in Numbers/Integers/TreeMod) that tree-like representation o...	emakarov
2007-10-03	BigZ now are proved	thery
2007-10-02	Now NMake is proved	thery
2007-09-28	Creation of a new token PATTERNIDENT (?ident) for intro patterns, so	glondu
2007-09-21	- Fixing bug 1703 ("intros until n" falls back on the variable name when	herbelin
2007-07-30	mul and sqrt	thery
2007-07-25	Pattern matching sur BigN.N13 manquant dans les fonctions do_norm_n et	notin
2007-07-24	proof of compare added	thery
2007-07-18	A generic preprocessing tactic zify for (r)omega	letouzey
2007-07-18	J'ai enlevé un fichier qui était en double. Merci à Pierre pour avoir	aspiwack
2007-07-12	Proof for sub	thery
2007-07-12	normalisation (by closure) was not performed under fixpoints	barras
2007-07-12	Proof for succ, add, pred	thery
2007-06-20	ajout de head0 et tail0 en natif	bgregoir
2007-06-19	safe_shift correct recursion	thery
2007-06-19	safe_shift recursion	thery
2007-06-19	safe_shift recursion	thery
2007-06-19	Adding function is_even, safe_shiftl, safe_shiftr	thery
2007-06-19	genN.ml sync	thery
2007-06-18	Correct height computation	thery
2007-06-06	tail0	thery
2007-05-30	mul_norm for Q fixed	thery
2007-05-21	Added Z and Q implementations with int31.	aspiwack
2007-05-21	add_mul_pos uses int31 only	thery
2007-05-15	pos_mod fixed	thery
2007-05-15	Correction de sqrt312 (racine carree d'un nombre represente comme un	aspiwack
2007-05-11	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack