coq - the Coq proof assistant

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