coq - The formal proof system

Age	Commit message (Expand)	Author
2007-05-11	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack
2007-04-29	Multiples changements autour des implicites :	herbelin
2007-04-28	Ajout de la possibilité de faire référence dans certains cas à un nom	herbelin
2007-04-28	Ajout de la possibilité d'utiliser les evars dans apply_in et elim_in.	herbelin
2007-04-27	fixed glitch in escape	corbinea
2007-04-26	fin des conclusions multiples	corbinea
2007-04-25	New keyword "Inline" for Parameters and Axioms for automatic	soubiran
2007-04-18	debug plus poussé induction dépendante	corbinea
2007-04-18	- Correction d'un bug de make_clenv_binding_apply révélé par le commit 9771	herbelin
2007-04-16	Export de simplest_eapply, utilisé dans la contrib interface	notin
2007-04-16	fix bug with dependent inductive families	corbinea
2007-04-16	Suite unification apply et eapply (l'un et l'autre profite maintenant	herbelin
2007-04-15	Essai de partage de code entre apply et eapply	herbelin
2007-04-13	Proposition de correction pour le bug #1173 (ou du moins pour un	herbelin
2007-04-13	Nettoyage des tactiques basées sur "simpl" (delta-réduction cachant	herbelin
2007-04-02	Extension to the general sequence operator (tactical). Now in addition to ...	emakarov
2007-03-30	Changement mineur du comportement de 'rewrite .. in * \|-': si le	notin
2007-03-19	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau
2007-03-15	Suppression argument pattern_source du case_info (code jamais utilisé)	herbelin
2007-03-13	Correction bug #1439 (comportement de replace by)	notin
2007-02-24	Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...	herbelin
2007-02-22	Ajout fonction clenv_conv_leq pour résoudre les pbs de la forme	herbelin
2007-02-21	Correction typo liée au commit 8779 (levait une anomalie)	herbelin
2007-02-15	Réparation absence d'interprétation des liaisons vers listes	herbelin
2007-02-13	Réactivation du filtrage d'ordre 2 dans ltac qui avait cessé de	herbelin
2007-02-09	bugfix suffices	corbinea
2007-02-09	Report de la révision r9605 de la branche v8.1 vers le trunk (abstract récu...	notin
2007-02-06	Report de la révision 9599 de la v8.1 dans le trunk	notin
2007-02-01	Suppression de code mort	notin
2007-01-31	redirection of errors in coqide + dynamic warning printer (needed for tm_egg)	corbinea
2007-01-29	bugfix for suffices (support for open head)	corbinea
2007-01-29	finalized suffices	corbinea
2007-01-28	"suffices" implemented + syntax cleanup	corbinea
2007-01-25	decl mode: anonymous facts	corbinea
2007-01-22	Correction du bug #1315:	notin
2007-01-22	changes in declarative language : by term using tactic	corbinea
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