coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Projections	herbelin	2003-09-03
*	Added a test for Functional Induction.	courtieu	2003-06-21
*	Test backtracking	herbelin	2003-05-22
*	Nouveaux tests	herbelin	2003-05-21
*	Corrige Bug (PR#290)	coq	2003-05-05
*	Ce que Try récupère	herbelin	2003-04-27
*	Débranchement des tests output qui sont faussés par le traducteur	herbelin	2003-04-15
*	indentation	herbelin	2003-03-29
*	* empty log message *	barras	2003-03-14
*	MAJ	herbelin	2003-03-04
*	fixing a typo in the new Funinv.v test in test-suite/success	courtieu	2003-02-28
*	Adding tests for the "functional induction" facility.	bertot	2003-02-27
*	commentaire	coq	2003-02-06
*	MAJ syntaxe modules + nouveau fichier mod_decl qui explique tout	coq	2003-01-31
*	Pb de parenthèse dans "Check (S (plus O O))"	herbelin	2003-01-30
*	MAJ pour Reg	desmettr	2003-01-28
*	* empty log message *	barras	2003-01-22
*	* empty log message *	herbelin	2003-01-20
*	Tests ltac	herbelin	2003-01-19
*	Il ne doit plus y avoir de preuves non terminées à la sortie du fichier	herbelin	2003-01-19
*	* empty log message *	herbelin	2003-01-16
*	Problème de désynchronisation des variables du type et du corps d'un point-...	herbelin	2003-01-15