coq - The formal proof system

Age	Commit message (Expand)	Author
2007-03-19	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau
2007-02-24	Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...	herbelin
2007-02-21	Utilisation de l'environnement pour l'affichage de certains messages d'erreurs	herbelin
2007-01-24	Tentative amélioration messages d'erreur prédicat d'élimination (cf notamment	herbelin
2006-10-05	Correction d'un bug dans l'unification: lors de l'unification d'un meta m et ...	notin
2006-05-23	Nouvelle implantation du polymorphisme de sorte pour les familles inductives	herbelin
2006-02-07	Messages nth branche	herbelin
2006-02-07	Amélioration des messages d'erreurs de tacred; unfold considère maintenant le	herbelin
2006-01-30	Message d'erreur si l'inductif d'une clause "in" d'un match n'a pas la	herbelin
2006-01-11	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin
2005-12-26	Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...	herbelin
2005-12-17	Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...	herbelin
2005-12-17	Création d'un type d'erreur RecursionSchemeError distinct de InductiveError ...	herbelin
2005-11-08	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin
2005-11-02	Types inductifs parametriques	mohring
2004-12-03	Amélioration message d'erreur v8	herbelin
2004-10-17	Semble raisonnable de distinguer les noms aussi dans cant_apply	herbelin
2004-09-15	hiding the meta_map in evar_defs	barras
2004-09-03	deplacement de clenv vers pretyping	barras
2004-09-03	premiere reorganisation de l\'unification	barras
2004-08-23	Correction bug #830 : les noms des implicites temporaires étaient inconnus a...	herbelin
2004-08-06	Amélioration message d'erreur objet de récursion de type non inductif	herbelin
2004-07-16	Nouvelle en-tête	herbelin
2004-07-13	bug #790: better error_not_clean	barras
2004-02-28	Traduction 'Cases' en pattern-matching	herbelin
2004-02-18	- fixed the Assert_failure error in kernel/modops	barras
2004-02-04	Boite autour des quote pour eviter un retour a la ligne apres le premier guil...	herbelin
2004-02-03	Protection contre noms de variable indefinis et guillemets autour des constr	herbelin
2003-11-29	Utilisation nom dans message d'erreur implicite pas trouve	herbelin
2003-11-04	Amelioration message d'erreur	herbelin
2003-09-22	message d'erreur de garde des cofix	barras
2003-09-06	Paramétrisation vis à vis de existential_key	herbelin
2003-03-31	Restauration de make_all_different (disparu depuis version 1.74) car sinon de...	herbelin
2003-03-29	Mise en place de 'Implicit Variable' (variante du 'Reserve' de mizar)	herbelin
2003-03-12	* empty log message *	barras
2002-12-21	Légère amélioration des messages d'erreur des with-bindings et des Rewrite	herbelin
2002-12-19	suite du commit precedent	barras
2002-09-03	pretyping/pretyping.ml	herbelin
2002-08-13	Renoncement à distinguer les types "constr" et "types"; nettoyage	herbelin
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2002-04-10	Amélioration des messages d'erreurs concernant l'inférence des implicites	herbelin
2001-12-21	Un ++ au lieu d'un ;	herbelin
2001-12-18	Nettoyage exceptions liées au vieux Case	herbelin
2001-12-13	compat ocaml 3.03	filliatr
2001-11-29	nouvel algo de conversion plus uniforme	barras
2001-11-21	Amélioration message Cases	herbelin
2001-11-21	Amélioration messages d'erreur arité incorrecte (notamment record)	herbelin
2001-11-12	Suites modifs du noyau. Univ devient purement fonctionnel.	barras
2001-11-05	GROS COMMIT:	barras