coq - The formal proof system

Age	Commit message (Expand)	Author
2006-07-12	Documentation machine virtuelle	herbelin
2006-07-12	Correction incohérence parsing de %delim dans les motifs	herbelin
2006-07-11	Ajout de quelques Arguments Scope pour simuler la récursivité du scope Rfun...	herbelin
2006-07-11	Ajout de quelques Arguments Scope pour simuler la récursivité du scope rome...	herbelin
2006-07-11	MAJ doc/refman	notin
2006-07-11	MAJ	herbelin
2006-07-11	Documentation de lazymatch et des extensions de idtac et fail	herbelin
2006-07-11	Utilisation du mot-clé lazymatch pour le match paresseux (à défaut d'avoir...	herbelin
2006-07-10	+functional inversion now takes the function to invert as an optional argument.	jforest
2006-07-09	Argument Scope de list déplacé dans List.v	herbelin
2006-07-07	Correction bug 1172 + correction en passant de la taille des paramètres de f...	herbelin
2006-07-07	Correction bug 1172 + correction en passant de la taille des paramètres de f...	herbelin
2006-07-07	MAJ	herbelin
2006-07-07	Documentation Declare Implicit Tactic, Print Canonical Projections, ... + lé...	herbelin
2006-07-07	MAJ du manuel de référence (modules+fixpoints+pose proof)	notin
2006-07-06	Documentation Whelp	herbelin
2006-07-06	MAJ	herbelin
2006-07-06	Typo	herbelin
2006-07-06	Quelques Hint inutiles	herbelin
2006-07-06	Remplacement VernacDebug par VernacSetOption (suite)	herbelin
2006-07-06	Suite remplacement VernacDebug par VernacSetOption	herbelin
2006-07-05	MAJ	herbelin
2006-07-05	MAJ doc	herbelin
2006-07-05	Branchement de 'Debug On/Off' sur le mécanisme standard d'option et donc, re...	herbelin
2006-07-05	Ajout taclevel	herbelin
2006-07-05	Documentation Print Ltac qualid; documentation du debugger de ltac.	herbelin
2006-07-05	Branchement de 'Debug On/Off' sur le mécanisme standard d'option et donc, re...	herbelin
2006-07-05	Nettoyage code mort	herbelin
2006-07-05	Correction typo + ajout Arabic Supplement	herbelin
2006-07-05	Use typing informations while defining graphs for Function.	jforest
2006-07-05	Précisions sur l'Unicode reconnu; typo; ajout Example, Proposition, Corollary.	herbelin
2006-07-05	Mise à jour scopes prédéfinis et Tactic Notation pour tacticals	herbelin
2006-07-05	Documentation 'external'	herbelin
2006-07-05	Correcting for bug #1167	jforest
2006-07-04	functional inversion now takes a quatified hypothesis as first argument	jforest
2006-07-04	Que le niveau 100 soit associatif à droite dans operconst et à gauche dans ...	herbelin
2006-07-04	Doc Print Grammar pattern	herbelin
2006-07-04	Documentation or-pattern	herbelin
2006-07-04	Documentation or-pattern	herbelin
2006-07-04	Ajout cible refman-quick qui teste la compilation sans faire les index, toc e...	herbelin
2006-07-04	adding comments and cleaning code	jforest
2006-07-04	Typo dans le manuel de référence	notin
2006-07-04	Ajout espacement autour des symboles latex a l'attention de 'hevea -nosymb' +...	herbelin
2006-07-04	- completely new version of "functional inversion" using inversion on	jforest
2006-07-04	MAJ du manuel de référence	notin
2006-07-03	Test des motifs disjonctifs multiples	herbelin
2006-07-03	Extension des motifs disjonctifs au cas de disjonction de motifs multiples	herbelin
2006-07-03	Mise à jour (avec retard) des niveaux de la table default_pattern_levels	herbelin
2006-07-03	MAJ manuel de référence	notin
2006-06-29	forgot a file	jforest