coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	maj	coq	2004-12-08
*	Ajout bug do_restrict_hyp	herbelin	2004-12-08
*	Correction d'un bug historique de do_restrict_hyps + code mort	herbelin	2004-12-08
*	Correction d'un bug historique de do_restrict_hyps + code mort	herbelin	2004-12-08
*	Bugs dans la déclaration du type du terme filtré si non défini	herbelin	2004-12-08
*	Bug nom exception	herbelin	2004-12-08
*	maj	coq	2004-12-07
*	maj	coq	2004-12-07
*	* added subst_evaluable_reference	sacerdot	2004-12-07
*	The type Pattern.constr_label was isomorphic to Libnames.global_reference.	sacerdot	2004-12-07
*	Uniformisation du nom d'entrée openconstr en le nom du type open_constr	herbelin	2004-12-06
*	Erreur commit précédent	herbelin	2004-12-06