coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à un...	herbelin	2003-01-15
*	Export M + Module M <: SIG	coq	2003-01-09
*	Require SplitAbsolu -> Require Rfunctions pour compatibilite avec la nouvelle...	desmettr	2002-12-12
*	Add an example with Ring.	bertot	2002-12-09
*	MAJ sur MAJ	herbelin	2002-12-02
*	Remplacement de Syntactic Definition par Notation	herbelin	2002-12-02
*	MAJ	herbelin	2002-11-25
*	MAJ	herbelin	2002-11-24
*	Remplacement de Syntactic Definition par Notation	herbelin	2002-11-24
*	Test de la correction d'un bug soumis par Dachuan Yu	herbelin	2002-11-06
*	Des critères plus fins d'analyse des implicites automatiques; meilleur affic...	herbelin	2002-10-29
*	Omega échouait à effacer les hypothèses à contenu arithmétique lorsque c...	herbelin	2002-10-23
*	Parenthèses manquantes pour se conformer à la doc (et au nouveau PeanoSynta...	herbelin	2002-10-21
*	Parseur pour n>20 dans nat plus disponible	herbelin	2002-10-16
*	correcting the treatment of many tactics that use quant_hyp in file xlate.ml	bertot	2002-10-06
*	Adding the congruence closure tactics (CC and CCsolve).	corbinea	2002-10-01
*	Encore quelques rangements dans Nametab + petits trucs	coq	2002-09-27
*	Changement de sémantique de Remark : maintenant un global comme les autres	herbelin	2002-09-21
*	Correction	coq	2002-08-21
*	Encore quelques tests sur modules...	coq	2002-08-16
*	Test for redundant clauses	herbelin	2002-08-15
*	Test affichage optimal des coercions	herbelin	2002-08-14