coq - The formal proof system

Age	Commit message (Expand)	Author
2006-12-26	Report correction bug #1289 dans trunk (r9435 pour branche v8.1)	herbelin
2006-12-22	remplacement d'un test d'egalite par un test de convertibilite dans injection...	jforest
2006-12-13	Dépliage du terme d'induction avant suppression quand celui-ci est un	herbelin
2006-12-12	Correction bug #1041 (double cause : non évitement des noms existants en	herbelin
2006-12-11	Changement dans le kernel :	bgregoir
2006-11-19	Raffinement de l'unification de "apply": mémorisation de certains	herbelin
2006-11-10	Ajout de dépliage de l'énoncé, si besoin est, dans apply in	herbelin
2006-11-10	Correction d'un bug refine	herbelin
2006-11-01	Quick hack to solve to complexity issue in function mark_occur	herbelin
2006-10-31	Retour sur la modification apportée en r9289, et nouvelle correction du bug ...	notin
2006-10-27	simplif de la partie ML de ring/field	barras
2006-10-26	Affichage d'un message d'erreur losque qu'une relation n'a pas été déclar�...	notin
2006-10-26	Petit bug apply in	herbelin
2006-10-25	Correction d'une tentative incorrecte (révision 9266) de clarification	herbelin
2006-10-24	Insère une coercion vers Sortclass dans 'contradiction' si nécessaire	herbelin
2006-10-24	Extension de la primitive ltac fresh pour qu'elle accepte une liste de	herbelin
2006-10-24	Ajout de la tactique "apply in".	herbelin
2006-10-24	Interprétation du terme comme type dans 'change' si pas de 'with' (pour bén...	herbelin
2006-10-23	Fixed "Show intros" which did not look at hypothesis.	courtieu
2006-10-20	Correction du bug #1255 (réécriture setoid sous un produit)	notin
2006-10-16	affichage des ... dans les scripts	barras
2006-10-05	revision de la semantique de rewrite ... in <clause>. details dans la doc	letouzey
2006-10-03	Changement de comportement du [rewrite ... in H]: Coq échoue si H	notin
2006-10-03	Retour sur la suppression du pf_nf (trop d'exemples utilisent avec	herbelin
2006-10-01	Une passe sur l'injection et la discrimination...	herbelin
2006-09-30	Suppression de la comparaison (inutile) des paramètres globaux des	herbelin
2006-09-26	mise a jour du nouveau ring et ajout du nouveau field, avant renommages	barras
2006-09-26	fixed error mesg in decl mode	corbinea
2006-09-25	Permet a un unfold de recevoir ses occurences a travers une variable Ltac.	letouzey
2006-09-23	Correction bug #1229 (toplevel "unresolved evar" fled through	herbelin
2006-09-22	Ajout d'une valeur VList dans tacinterp pour permettre de cabler des	herbelin
2006-09-21	Visibilité des Rewrite Hint dès le chargement du module, sans nécessiter s...	herbelin
2006-09-20	Declarative Proof Language: main commit	corbinea
2006-09-12	Indentation + svnprop	notin
2006-09-01	Correction bug d'ordonnancement des hyps d'induction dans induction/destruct	herbelin
2006-08-28	improve the amount of information given by the Ltac tactic debugger	bertot
2006-08-23	Bug in replace tactics introduced in r9073 (overlap between replace .. with a...	jforest
2006-08-22	Forgot a file in previous commit	jforest
2006-08-22	+ Changing "in <hyp>" to "in <clause>" (no at, no InValue and no	jforest
2006-08-17	corrects an error in the substitution of module paths inside tactics:	bertot
2006-07-28	Reparation bug Show intros: les hypothèses introduites précédemment	courtieu
2006-07-20	Correction du bug #1116	jforest
2006-07-18	amelioration du comportement de induction (retour a la version V8.0)	jforest
2006-07-05	Correcting for bug #1167	jforest
2006-06-27	Backtrack sur l'introduction de contraintes sur l'absence des 'ident' dans l'...	herbelin
2006-06-23	Suite utilisation hyp au lieu ident: donne la localisationn	herbelin
2006-06-23	Correction ident -> hyp pour dinterprÃ©ter des identificateurs devant Ãªt...	herbelin
2006-06-23	Préservation compatibilité interprétation quantified hypothesis (provisoir...	herbelin
2006-06-22	Nettoyage, uniformisation	herbelin
2006-06-21	Harmonisation de l'interprétation des intropattern	herbelin