coq - The formal proof system

Age	Commit message (Expand)	Author
2007-10-03	Ajout de eelim, ecase, edestruct et einduction (expérimental).	herbelin
2007-10-01	Complément nécessaire aux révisions 10156 et 10157	herbelin
2007-09-28	Modification of the Scheme command.	vsiles
2007-09-21	curpat_ty was in a smaller context	msozeau
2007-09-20	Changed the definition of Nminus in BinNat.v by removing comparison.	emakarov
2007-09-17	Raffinement de l'algorithme d'inférence de type	herbelin
2007-09-15	* Adding compability with ocaml 3.10 + camlp5 (rework of	letouzey
2007-09-14	Correction du bug #1679 (congruence) et ajout test-suite	corbinea
2007-09-06	errors in recdef.ml4:	bertot
2007-09-06	this should fix a problem described in a message by Dufourd on July 30th, 2007	bertot
2007-08-31	fin de la correction de Function	jforest
2007-08-31	correction bug d'efficacite dans Function	jforest
2007-08-30	Oubli dans commit 10102...	herbelin
2007-08-29	- Débogueur: positionnement de set_detype_anonymous pour ne pas	herbelin
2007-08-27	Oubli dans la révision 10098 (nettoyage body_of_type)	herbelin
2007-08-27	Suppression des type_app et body_of_type qui alourdissent inutilement le code	herbelin
2007-08-26	Fix bug on wellfounded defs with constant parameters and dependencies on the ...	msozeau
2007-08-26	Fix de Bruijn bug in wf definitions.	msozeau
2007-08-26	Fix evars bug in mutual fixpoints with implicit types and bug in inequalities...	msozeau
2007-08-16	Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;	notin
2007-08-08	Fix dependency bugs due to Program modules renamings.	msozeau
2007-08-07	Move Program tactics into a proper theories/ directory as they are general pu...	msozeau
2007-07-24	fixed bug 1448 and 1674	barras
2007-07-24	fixed bug 1675: computing carrier from the relation type was not right	barras
2007-07-24	Declarative language: fixed the generation of fixpoints for induction proofs.	corbinea
2007-07-19	Documentation of Program and its tactics, fix enormous interaction bug due to...	msozeau
2007-07-18	A generic preprocessing tactic zify for (r)omega	letouzey
2007-07-16	Generalized CAMLP4USE for pp dependencies	corbinea
2007-07-13	some more useless constant in const_omega	letouzey
2007-07-13	Beginning of a reorganisation of the ml part for romega:	letouzey
2007-07-13	removing a warning at compilation time	jforest
2007-07-12	Deletion of contrib/extraction/test	letouzey
2007-07-12	normalisation (by closure) was not performed under fixpoints	barras
2007-07-12	port de r9968: bug avec les ring calculatoires	barras
2007-07-12	An optimization to simplify generated obligations removing unnecessary let-in's.	msozeau
2007-07-12	Fix bug when adding progs with no obligations	msozeau
2007-07-12	Remove dead modules in Subtac.	msozeau
2007-07-12	Cleanup, use Util list functions when possible	msozeau
2007-07-11	Slight cleanup of refl_omega.ml : in particular it uses now list	letouzey
2007-07-10	Big reorganization of romega/ReflOmegaCore.v: towards a modular	letouzey
2007-07-09	Improvements / Bug fixes for ROmega	letouzey
2007-07-06	minor bug correction (continuing r 9943)	jforest
2007-07-06	Adding a syntax for "n-ary" rewrite:	letouzey
2007-07-06	sequel to commit 9952: forgot to adapt xlate to the new n-ary rename	letouzey
2007-07-06	extension of the rename tactic: the following is now allowed:	letouzey
2007-07-06	New intro pattern "@A", which generates a fresh name based on A.	glondu
2007-07-05	Minor bug correction in Function. Non terminating Function e.g.	jforest
2007-07-02	Better handling of aliases, add command to solve a particular obligation.	msozeau
2007-06-26	killing some more non-exhaustive patterns	letouzey
2007-06-21	Correction de plusieurs bugs de l'export XML (utilisation d'un type de	herbelin