coq - The formal proof system

Age	Commit message (Expand)	Author
2002-11-04	Un fichier a utiliser via Drop pour le debug de l'extraction.	letouzey
2002-11-04	ajout d'une entrée au makefile pour faire toutes les theories sauf les reals	letouzey
2002-11-04	ajout d'un printer pour les global_reference	letouzey
2002-11-03	Ajout delimiteurs dans les motifs de Cases	herbelin
2002-11-03	Moulinette	herbelin
2002-11-03	Divers	herbelin
2002-11-01	maj	filliatr
2002-10-31	L'extraction c'est magic cvs -n up	letouzey
2002-10-31	maj	filliatr
2002-10-30	Désagglutination du squelette de la notation et de sa précédence	herbelin
2002-10-30	Optimisation du choix des niveaux intermédiaires dans une notation complexe	herbelin
2002-10-29	Bugs	herbelin
2002-10-29	Des critères plus fins d'analyse des implicites automatiques; meilleur affic...	herbelin
2002-10-29	Mais laisser la syntaxe (!id) aussi disponible !	herbelin
2002-10-29	Préservation de la cohérence du cache en cas d'erreur au chargement	herbelin
2002-10-29	Parenthèse non obligatoires autour de !id sans argument	herbelin
2002-10-29	Prise en compte let-in	herbelin
2002-10-29	maj	filliatr
2002-10-28	Des critères plus fins d'analyse des implicites automatiques; meilleur affic...	herbelin
2002-10-28	maj	filliatr
2002-10-26	code mort	herbelin
2002-10-23	Clarification changements autour de Remark/Fact/Local	herbelin
2002-10-23	Ajout de la syntaxe "Theorem f [binders] : t", comme pour Definition et Local	herbelin
2002-10-23	Omega échouait à effacer les hypothèses à contenu arithmétique lorsque c...	herbelin
2002-10-23	Le test de redondance d'une règle était trop fort	herbelin
2002-10-23	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-22	MAJ	herbelin
2002-10-22	Redéplacement de + (sum) et * (prod) au niveau de + et * de l'arithmétique;...	herbelin
2002-10-22	Correction d'une incompatibilité de nommage introduite lors du commit préc�...	herbelin
2002-10-22	maj	filliatr
2002-10-21	Ajout d'un suffixe "as [ names ]" pour nommer manuellement les	herbelin
2002-10-21	Mise en transparence des schémas d'induction bien-fondée sur Set	herbelin
2002-10-21	NewDestruct/NewInduction acceptent l'option "using"	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	Prise en compte des délimiteurs dans les motifs de Cases	herbelin
2002-10-21	Parenthèses manquantes pour se conformer à la doc (et au nouveau PeanoSynta...	herbelin
2002-10-21	Bug qui empêchait "0" d'être parenthèsé	herbelin
2002-10-19	Meilleure lisibilité grâce à tclTHENLIST	herbelin
2002-10-19	Réparation bug #180	herbelin
2002-10-19	Ajout d'infixes	herbelin
2002-10-18	Et 48, et 80, et 81, et 91, et 95, ... pour accommoder toujours plus de contribs	herbelin
2002-10-17	Bugs dans la factorisation des règles de parsing de "{ ... } * ..."	herbelin
2002-10-17	Moins de restriction sur le commit 1.5	herbelin
2002-10-17	Parsing des entiers de nat jusqu'à 29 pour accommoder certaines contribs	herbelin
2002-10-16	Réparation du mécanisme des infixes quand ils commencent par une lettre	herbelin
2002-10-16	Parseur pour n>20 dans nat plus disponible	herbelin
2002-10-16	maj	filliatr
2002-10-15	nom de fonction plus simple	barras