coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	bug de PP des fix (coqbugs #574)	barras	2004-03-24
*	Nouvel exemple; correction du contexte du précédent	herbelin	2004-03-13
*	Corrections	herbelin	2004-03-12
*	Test l'interprétation des scopes	herbelin	2004-03-11
*	Ajout exemple Inst	herbelin	2004-03-11
*	Ajout vieil exemple de coq-club	herbelin	2004-03-11
*	Ajout d'un vieil exemple de N. Magaud	herbelin	2004-03-11
*	Ajout bug #540	herbelin	2004-03-11
*	the output the parser should produce now	bertot	2004-03-06
*	changed the test for obj_magic.v to be less sensitive to changes	bertot	2004-03-06
*	modif des fixpoints pour que si on donne une notation au produit, les pts fix...	barras	2004-03-05
*	Exemple de Frederic	herbelin	2004-02-28
*	Ajout test synthese du predicat a partir du cast d'un filtrage avec dependances	herbelin	2004-02-27
*	New version of Functional Scheme and functional induction. Deals with	coq	2004-02-09
*	Test dependencies in constructors	herbelin	2004-02-06
*	Ajout filtrage sur motifs dépendants dans des inductifs différents	herbelin	2004-02-06
*	Vérification de la prise en compte des termes de type non inductif	herbelin	2004-02-04
*	[ -d ... ] au lieu de [ -f ... ] sur commit précédént	herbelin	2004-01-01
*	Protection contre l'echec des tests parser pour la distrib	herbelin	2003-12-27
*	Suppression en v8	herbelin	2003-12-27
*	BUG	herbelin	2003-12-24
*	Bug commit precedent	herbelin	2003-12-23
*	Renommages des hypotheses transformees car en raison des possibles dependance...	herbelin	2003-12-23
*	ajout test de non-regression Clear d'une def locale	barras	2003-12-17
*	Ajout exemple Yves	herbelin	2003-12-12
*	Pour eviter d'avoir un gros type dans Set	herbelin	2003-12-05
*	ground->firstorder, cc-> congruence, CC final commit	corbinea	2003-11-29
*	Simplest Demo on modules	coq	2003-11-28
*	removal of CC.v lemata in cc (deprecated)	corbinea	2003-11-26
*	CC: added injection theory	corbinea	2003-11-25
*	Niveau V8	herbelin	2003-11-13
*	Fermeture de la section maintenant necessaire	herbelin	2003-11-13
*	Passage a un SStream predicatif	herbelin	2003-11-13
*	Test Generalize	herbelin	2003-11-09
*	MAJ	herbelin	2003-10-27
*	Test obsolete	herbelin	2003-10-14
*	Cleaning	herbelin	2003-10-13
*	Logic_TypeSyntax disparu	herbelin	2003-10-11
*	* empty log message *	herbelin	2003-10-10
*	changement nouvelle syntaxe (pt fixes)	barras	2003-10-10
*	Cacher les .v8	herbelin	2003-10-10
*	Teste interaction ltac et modules	herbelin	2003-10-08
*	Ajout exemple parametres implicites	herbelin	2003-10-08
*	Test Conjecture	herbelin	2003-10-08
*	Correction du bug 335 et Export/Require Export dans un module	coq	2003-10-07
*	Traduction des tests success et test en v8	herbelin	2003-10-02
*	Correction bug 328	coq	2003-09-23
*	test d'implicite incorrect depuis que eq porte sur Type	barras	2003-09-23
*	L'exemple phare de modules - simplifie pour TPHOLs	coq	2003-09-22
*	Check local definitions in context of inductive types	herbelin	2003-09-06