coq - The formal proof system

Age	Commit message (Expand)	Author
2006-01-20	Ajout de la contrainte de résoudre l'assertion dans 'assert by'	herbelin
2006-01-20	Test bug 983	herbelin
2006-01-20	* empty log message *	barras
2006-01-19	maj	coq
2006-01-19	Conséquences supplémentaires de la fin du support v7	herbelin
2006-01-19	Export eassumption	herbelin
2006-01-19	Extended Unicode support	herbelin
2006-01-19	Correction associativité de IF et exists (visible à l'affichage uniquement ...	herbelin
2006-01-18	maj	coq
2006-01-18	Retrait de 'by' comme mot-clé en espérant qu'il n'y aura pas d'interférenc...	herbelin
2006-01-18	Recursive Definition now supports functions with more than one argument.	coq
2006-01-17	maj	coq
2006-01-16	maj	coq
2006-01-16	dans la liste des cmo pour dev/printers.cma, manquait proofs/tacexpr.cmo	letouzey
2006-01-16	Version préliminaire d'inversion de la compilation du filtrage	herbelin
2006-01-16	Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq	herbelin
2006-01-16	Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq choisir un nom	herbelin
2006-01-16	* empty log message *	coq
2006-01-16	Code redondant	herbelin
2006-01-16	Correction dans vernac_exact_proof -- jmn	coq
2006-01-16	- Tactic "assert" now accepts "as" intro patterns and "by" tactic clauses	herbelin
2006-01-16	cvs ci -m "Passage à la limite dans les intro-pattern de n-uplets"	herbelin
2006-01-15	maj	coq
2006-01-15	Ajout de nouvelles plages de symboles unicode; prise en compte des indices un...	herbelin
2006-01-15	Bug (code prévu pour iso-latin et non utf-8)	herbelin
2006-01-15	Test utf-8	herbelin
2006-01-14	maj	coq
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