coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Une entrée spéciale "annot" pour les piquants	herbelin	2002-12-15
*	Ajout syntaxe '>'	herbelin	2002-12-15
*	Ajout syntaxe '>'	herbelin	2002-12-15
*	Pas d'associativite pour =_D	herbelin	2002-12-15
*	Compatibilite times1 (suite)	herbelin	2002-12-10
*	Nouvelle preuve de times_convert pour nouvelle définition de times	herbelin	2002-12-09
*	Compatibilité times1	herbelin	2002-12-07
*	Un axiome en attendant la mise a jour de la preuve de times_convert	herbelin	2002-12-06
*	Amélioration sensible de l'efficacité de la multiplication	herbelin	2002-12-06
*	Essai d'introduction d'un scope des types	herbelin	2002-12-03
*	Z_scope doit annuler l'affichage de = entre	herbelin	2002-12-02
*	Re-échappement des \ et " dans les token string	herbelin	2002-11-29
*	Simplification	herbelin	2002-11-28
*	Essai de suppression du caractere d'echappement des string	herbelin	2002-11-28
*	Plus de précisions	herbelin	2002-11-28
*	cond_pos -> cond_positivity pour cause de conflit avec posreal...	desmettr	2002-11-27
*	Réorganisation de la librairie des réels	desmettr	2002-11-27
*	Retour sur associativité à droite de * pour compatibilité de prod	herbelin	2002-11-27
*	Ne pas cacher les Metas d'une notations, ils peuvent être liant dans	herbelin	2002-11-26
*	MAJ	desmettr	2002-11-26
*	Theorie 'light' des réels	desmettr	2002-11-26
*	Explicitation de NONA car sinon LEFTA par défaut; déplacement dans 5	herbelin	2002-11-26
*	Plus d'indication pour le gestionnaire de niveaux	herbelin	2002-11-26
*	Correction affichage entiers en cas d'échec	herbelin	2002-11-26
*	Bug ProjSn + retour de "Notation" pour déclarer les définitions syntaxiques	herbelin	2002-11-26
*	Bug niveau	herbelin	2002-11-26
*	Rétablissement affichage des entiers de nat	herbelin	2002-11-25
*	Retablissement SynDef Value/Error	herbelin	2002-11-25
*	Oubli	herbelin	2002-11-25
*	Traitement des parenthèses de nat au niveau du printer	herbelin	2002-11-24
*	Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...	herbelin	2002-11-24
*	Généralisation de l'utilisation de Notation	herbelin	2002-11-24
*	Remplacement de Syntactic Definition par Notation	herbelin	2002-11-24
*	Les parenthèses de la notation '(n)' maintemant mises par ML pour un meilleu...	herbelin	2002-11-20
*	Definition et proprietes de l'integrale de Riemann	desmettr	2002-11-18
*	Proprietes des fonctions en escalier	desmettr	2002-11-18
*	Réforme de l'interprétation des termes :	herbelin	2002-11-14
*	Oubli	herbelin	2002-11-14
*	JMeq now treated as an equality by tactics.	courant	2002-11-14
*	nettoyage preuve limit_comp	courant	2002-11-14
*	Un hack camlp4 qui marche à tous les coups pour continuer à parser '(n)' co...	herbelin	2002-11-07
*	Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pour	herbelin	2002-10-23
*	Re-déplacement de sum/sumor/sumbool et prod au niveaux 4 et 3 pour	herbelin	2002-10-23
*	Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;...	herbelin	2002-10-22
*	Mise en transparence des schémas d'induction bien-fondée sur Set	herbelin	2002-10-21
*	Niveau d'affichage sumor/sumbool incohérent avec le parsing	herbelin	2002-10-21
*	Prise en compte des délimiteurs dans les motifs de Cases	herbelin	2002-10-21
*	Et 48, et 80, et 81, et 91, et 95, ... pour accommoder toujours plus de contribs	herbelin	2002-10-18
*	Bugs dans la factorisation des règles de parsing de "{ ... } * ..."	herbelin	2002-10-17
*	Parsing des entiers de nat jusqu'à 29 pour accommoder certaines contribs	herbelin	2002-10-17