coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Ajout test bug 860	herbelin	2004-12-27
*	Remplacement du coeur d'omega (omega.ml) par la version plus générale utili...	herbelin	2004-12-27
*	Remplacement du coeur d'omega (omega.ml) par la version plus gnrale utilise p...	herbelin	2004-12-27
*	maj	coq	2004-12-26
*	maj	coq	2004-12-25
*	maj	coq	2004-12-25
*	Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...	herbelin	2004-12-25
*	Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...	herbelin	2004-12-25
*	maj	coq	2004-12-24
*	Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...	herbelin	2004-12-24
*	Typo	herbelin	2004-12-24
*	Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...	herbelin	2004-12-24
*	maj	coq	2004-12-23
*	MAJ coq v8	herbelin	2004-12-23
*	MAJ coq v8	herbelin	2004-12-23
*	Renommage de ocamldebug-v7 en ocamldebug-coq (pour passage à la v8)	herbelin	2004-12-23
*	Renommage de ocamldebug-v7 en ocamldebug-coq (pour passage à la v8	herbelin	2004-12-23
*	maj	coq	2004-12-22
*	Mecanisme d'affichage des types (notamment les conclusions des buts) typiquem...	herbelin	2004-12-22
*	maj	coq	2004-12-21
*	maj	coq	2004-12-20
*	maj	coq	2004-12-19
*	In_dec transparent (wish #902)	herbelin	2004-12-19
*	maj	coq	2004-12-18
*	maj	coq	2004-12-17
*	maj	coq	2004-12-16
*	maj	coq	2004-12-15
*	maj	coq	2004-12-14
*	maj	coq	2004-12-13
*	maj	coq	2004-12-12
*	maj	coq	2004-12-11
*	maj	coq	2004-12-10
*	Hugo fixed a bug of refine, and it revealed a bug of functional	coq	2004-12-10
*	maj	coq	2004-12-09
*	maj	coq	2004-12-09
*	Restauration type casted_open_constr pour tactique refine car l'unification n...	herbelin	2004-12-09
*	Correction du bug de build_initial_predicate a révèlé un autre bug dans ex...	herbelin	2004-12-09
*	Achèvement correction bug do_restrict_hys: ne pas inverser les arguments	herbelin	2004-12-09
*	Amélioration message localisation constructions et modules	herbelin	2004-12-09
*	Réactivation des tests output avec test aussi de la nouvelle syntaxe	herbelin	2004-12-09
*	Ajout d'une version nouvelle syntaxe	herbelin	2004-12-09
*	MAJ avec les particularités de l'afficheur v7 de la V8	herbelin	2004-12-09
*	Test d'affichage d'un Fix donné avec /n	herbelin	2004-12-09
*	Fichier non traductible (référence à des objets invisibles ce qui empêche...	herbelin	2004-12-09
*	Intégré à Implicit.v	herbelin	2004-12-09
*	Ajout suffixe 8 pour test en nouvelle syntaxe	herbelin	2004-12-09
*	Plus de statut spécial pour Remark	herbelin	2004-12-09
*	VOFILES aussi pour make depend	herbelin	2004-12-09
*	Désactivation du test du printer arithmétique v7	herbelin	2004-12-09
*	travail sur les types extraits	letouzey	2004-12-09