coq - The formal proof system

Age	Commit message (Expand)	Author
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey
2008-12-28	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin
2008-06-10	- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)	herbelin
2008-04-13	Bugs, nettoyage, et améliorations diverses	herbelin
2007-07-09	Improvements / Bug fixes for ROmega	letouzey
2007-05-20	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin
2006-11-16	suppression de code mort (avec bug de nom)	letouzey
2006-06-09	Bug suite déplacement Int.v dans ZArith	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 (mcanisme...	herbelin
2005-12-25	Adaptation des noms de OmegaLemmas aux noms de Z; traduction des noms v7 de Z...	herbelin
2005-12-02	Changement des named_context	gregoire
2005-11-08	Nettoyage suite à la détection par défaut des variables inutilisées par o...	herbelin
2005-02-18	Déboggueur et code mort	herbelin
2005-02-06	Nettoyage et documentation de Library	herbelin
2004-12-27	Utilisation d'entiers en précision arbitraire pour le noyau d'omega (cf #898)	herbelin
2004-12-27	Remplacement du coeur d'omega (omega.ml) par la version plus gnrale utilise p...	herbelin
2004-09-12	inclusion de meta_map dans evar_defs	barras
2004-07-16	Nouvelle en-tête	herbelin
2004-05-28	Retour sur amendement de l'interprétation mult sur nat (bug 743) car incompa...	herbelin
2004-05-07	Correction interprétation mult sur nat (bug 743), bug Oufo (mais Oufo est de...	herbelin
2004-03-04	Reparation ROmega V8/Omega ZERO/POS/NEG	mohring
2004-03-01	Protection d'un 'clear' qui peut etre dependant	herbelin
2003-12-24	La correction precedente a mis en evidence un defaut de l'utilisation de intr...	herbelin
2003-12-23	Renommages des hypotheses transformees car en raison des possibles dependance...	herbelin
2003-11-05	Déport des lemmes de Omega de ZArith vers OmegaLemmas	herbelin
2003-11-04	Extension de zarith	herbelin
2003-10-21	Construction des chemins de constantes plus robuste	herbelin
2003-09-26	Un peu plus de souplesse dans la globalisation des noms utilises par les tact...	herbelin
2003-06-10	Globalisation de ce qui n'etait pas encore globalise	herbelin
2003-05-19	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin
2003-04-17	commentaires	herbelin
2003-03-31	factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )	corbinea
2003-03-31	minus a changé d'emplacement -> omega pas content	letouzey
2003-03-12	* empty log message *	barras
2002-12-09	Problèmes et améliorations divers affichage	herbelin
2002-10-23	Omega échouait à effacer les hypothèses à contenu arithmétique lorsque c...	herbelin
2002-10-19	Meilleure lisibilité grâce à tclTHENLIST	herbelin
2002-10-19	Réparation bug #180	herbelin
2002-10-02	Omega can now elim hyps of type False. Therefore, it knows how to deal	courant
2002-09-24	Un peu (plus) d'ordre dans Nametab...	coq
2002-08-02	Modules dans COQ\!\!\!\!	coq
2002-06-03	Protection des tactiques contre l'utilisation sans le bon contexte de thories	herbelin
2002-05-29	Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...	herbelin
2002-04-11	Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.ml	herbelin
2002-02-28	Uniformisation convert_hyp	herbelin
2002-01-25	patch Omega (bug 129)	filliatr
2001-12-13	compat ocaml 3.03	filliatr
2001-11-05	GROS COMMIT:	barras
2001-10-09	Suppression des arguments sur les constantes, inductifs et constructeurs	barras