coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Application de la suggestion de Nicolas Magaud (#1060)	herbelin	2006-01-22
*	maj	coq	2006-01-21
*	Variable inutilisée	herbelin	2006-01-21
*	Backtrack commit précédent: la préservation de l'énoncé exact Acc_ind es...	herbelin	2006-01-21
*	Messages de idtac et fail peuvent maintenant être des listes de string, int ...	herbelin	2006-01-21
*	Ajout de la contrainte que l'assertion doit être complètement prouvée dans...	herbelin	2006-01-21
*	Messages de idtac et fail peuvent maintenant être des listes de string, int ...	herbelin	2006-01-21
*	Ajout niveau utilisateur de la tacticielle 'complete'; messages de idtac et f...	herbelin	2006-01-21
*	Déplacement de pr_arg et pr_opt de Ppconstr vers Util	herbelin	2006-01-21
*	Backtrack commit précédent (incompatible avec le choix de prendre Idtac com...	herbelin	2006-01-21
*	Préservation énoncé exact Acc_ind par choix nom 'a' comme paramètre de Acc	herbelin	2006-01-21
*	maj	coq	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-20
*	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-19
*	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-18
*	maj	coq	2006-01-17
*	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-16
*	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-15
*	maj	coq	2006-01-14
*	Code mort du traducteur	herbelin	2006-01-14
*	maj	coq	2006-01-13
*	Correction du bug #1055	coq	2006-01-13
*	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-12
*	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