coq - The formal proof system

Age	Commit message (Expand)	Author
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-22	maj	coq
2004-12-22	Mecanisme d'affichage des types (notamment les conclusions des buts) typiquem...	herbelin
2004-12-21	maj	coq
2004-12-20	maj	coq
2004-12-19	maj	coq
2004-12-19	In_dec transparent (wish #902)	herbelin
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	maj	coq
2004-12-10	Hugo fixed a bug of refine, and it revealed a bug of functional	coq
2004-12-09	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-08	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-07	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-06	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	Garder les cast semble décidément le meilleur moyen de rester synchrone ave...	herbelin
2004-12-06	Suppression des cast après avoir utiliser l'information de type (Tacinv envo...	herbelin
2004-12-06	Déplacement de la coercion vis à vis du but au niveau de Refine	herbelin