coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	- 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
*	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-11
*	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-10
*	maj	coq	2006-01-09
*	Suppression redondance coerce_to_id dans Pcoq et constrintern et déplacement...	herbelin	2006-01-09
*	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-08
*	maj	coq	2006-01-07
*	Réorganisation; suppression code mort; documentation	herbelin	2006-01-07
*	MAJ	herbelin	2006-01-07
*	maj	coq	2006-01-06
*	Petite modification de la gestion du '.' (jmn)	coq	2006-01-06
*	maj	coq	2006-01-05
*	* empty log message *	barras	2006-01-05