coq - The formal proof system

Age	Commit message (Expand)	Author
2006-01-14	Code mort du traducteur	herbelin
2006-01-13	maj	coq
2006-01-13	Correction du bug #1055	coq
2006-01-12	maj	coq
2006-01-12	Changing well founded induction to fix on accessibility proof in order	bertot
2006-01-12	Compatibilité prterm	herbelin
2006-01-11	maj	coq
2006-01-11	Test conflictuel - ajouté pour mémoire	herbelin
2006-01-11	Test or-patterns	herbelin
2006-01-11	Ajout test notation récursive	herbelin
2006-01-11	Suppression traducteur	herbelin
2006-01-11	remove warnings that were left in the directory contrib/interface	bertot
2006-01-11	removes several warnings in contrib/interface	bertot
2006-01-11	Résidus du traducteur v7 -> v8	herbelin
2006-01-11	Standardisation du nom de subst_raw en subst_rawconstr	herbelin
2006-01-11	Suite réorganisation des fonctions d'affichage	herbelin
2006-01-11	Standardisation du nom de subst_raw en subst_rawconstr	herbelin
2006-01-11	Résidus du traducteur v7 -> v8	herbelin
2006-01-11	Restructuration et simplification des fonctions d'affichage, de détypage	herbelin
2006-01-11	Ajout paramétricité du nom de la base de hint dans auto et trivial	herbelin
2006-01-11	Ajout paramétricité du nom de la base de hint dans auto et trivial	herbelin
2006-01-11	Suppression résidus code v7 et traducteur	herbelin
2006-01-10	Ajout de la longueur de l'arité des constructeurs dans one_inductive_body et...	herbelin
2006-01-10	maj	coq
2006-01-10	Détection var inutile par ocaml 3.09	herbelin
2006-01-09	maj	coq
2006-01-09	Suppression redondance coerce_to_id dans Pcoq et constrintern et déplacement...	herbelin
2006-01-08	maj	coq
2006-01-08	Prise en compte, enfin, du contexte des types de retour de ACases et RCases	herbelin
2006-01-08	Prise en compte de notations numérales définies au niveau utilisateur+ lég...	herbelin
2006-01-08	Prise en compte de notations numérales définies au niveau utilisateur + tra...	herbelin
2006-01-08	Enregistrement dans glob.dump des utilisations de notations numériques (qui ...	herbelin
2006-01-08	Automatisation de l'utilisation de token primitifs dans les motifs de filtrag...	herbelin
2006-01-08	Automatisation de l'utilisation de token primitifs dans les motifs de filtrage	herbelin
2006-01-08	Ajout rawconstr_of_aconstr	herbelin
2006-01-08	Fonctions de conversion rawconstr <-> cases_pattern	herbelin
2006-01-07	maj	coq
2006-01-07	Réorganisation; suppression code mort; documentation	herbelin
2006-01-07	MAJ	herbelin
2006-01-06	maj	coq
2006-01-06	Petite modification de la gestion du '.' (jmn)	coq
2006-01-05	maj	coq
2006-01-05	* empty log message *	barras
2006-01-05	Amelioration de l'elimination des preuves (bugs #1052 et #950-II) (jmn)	coq
2006-01-05	Test choix conflit afficheur de nombres selon la présence ou pas d'une coercion	herbelin
2006-01-05	* empty log message *	coq
2006-01-05	Suite révision 1.100 et synthèse optimale des 2 approches possibles: si la ...	herbelin
2006-01-05	Adding a man page for doqdoc (JMN)	coq
2006-01-04	maj	coq
2006-01-04	Suppression des coercions non seulement avant l'affichage des notations mais ...	herbelin