coq - The formal proof system

Age	Commit message (Expand)	Author
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
2004-12-06	Relâchement obligation d'une contrainte de type sur les Hole en position ter...	herbelin
2004-12-06	Code mort	herbelin
2004-12-06	Déplacement de la coercion vis à vis du but au niveau de Refine suite à ch...	herbelin
2004-12-06	Réparation bug #888 (les tactiques fix et cofix exigent autant de sous-buts ...	herbelin
2004-12-06	Ajout bug #888	herbelin
2004-12-06	Ajout bug #889	herbelin
2004-12-06	C'est trop compliqué de mettre à jour les types du metamap en passant sous ...	herbelin
2004-12-06	Inutile de réserver les notations à base de '{ }'	herbelin
2004-12-06	Commentaire	herbelin
2004-12-06	Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...	herbelin
2004-12-06	MAJ affichage nouvelle syntaxe	herbelin
2004-12-06	Commentaire	herbelin
2004-12-06	Bug (cf #892)	herbelin
2004-12-05	MAJ	herbelin
2004-12-05	MAJ changements ChoiceFacts	herbelin
2004-12-05	MAJ	herbelin
2004-12-05	Paramétrisation du domaine des axiomes de choix + ajout description = choice...	herbelin
2004-12-04	Bug 'set n in * \|-'	herbelin
2004-12-04	Failed in 8.0pl1	herbelin
2004-12-03	Orthographe!	herbelin
2004-12-03	Propagation du nom des hyps du prédicat de filtrage pour le message d'erreur...	herbelin
2004-12-03	Was failing in 8.0pl1	herbelin
2004-12-03	Amélioration message d'erreur v8	herbelin
2004-12-01	pp of nested fixpoints (dangling with/for)	barras
2004-11-30	Export pr_intro_pattern	herbelin
2004-11-29	UserError in reduce_to_*_ref	herbelin
2004-11-29	Complétion commit précédent	herbelin
2004-11-29	* empty log message *	gregoire