coq - The formal proof system

Age	Commit message (Expand)	Author
2007-05-21	Protection d'un warning par if_verbose	herbelin
2007-05-20	- Propagation des evars non résolues vers les with_bindings; permet par exemple	herbelin
2007-05-19	Backtrack sur l'effacement dans le contexte de but des lieurs	herbelin
2007-05-18	Interprétation des listes de VarArgType dans les notations faisant	herbelin
2007-05-18	Wish #1582 (3eme)	herbelin
2007-05-18	Quelques essais autour du wish implicite au rapport de bug #1582 (2eme)	herbelin
2007-05-18	Quelques essais autour du wish implicite au rapport de bug #1582	herbelin
2007-05-17	correction de bug dans Function et augmentation de la classe des fonctions su...	jforest
2007-05-17	Nettoyage et standardisation des messages d'erreurs.	herbelin
2007-05-17	Correction des bugs #1537 (anomalie sur signature incomplète) et #1536	herbelin
2007-05-17	Fixed bug #1540 (typo on name .coqide-gtk2rc)	herbelin
2007-05-16	Correction bug calcul des implicites en présence d'evars dans les types	herbelin
2007-05-16	- MAJ entêtes des fichiers produits par coq_makefile	herbelin
2007-05-15	Correction du pretty-printing des big-int (la sous-fonction get_height	aspiwack
2007-05-15	pos_mod fixed	thery
2007-05-15	Correction de sqrt312 (racine carree d'un nombre represente comme un	aspiwack
2007-05-15	corrections bug dans l'implem de int31	bgregoir
2007-05-11	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack
2007-05-11	Made some places in the reference manual clearer. Corrected	emakarov
2007-05-10	Prise en compte réversibilité des notations de la forme "Notation Nil := @n...	herbelin
2007-05-07	Correction du bug #1509	notin
2007-05-06	Nouveaux changements autour des implicites (notamment suite à	herbelin
2007-04-30	Modification syntaxe de Test	herbelin
2007-04-29	Orthographe en passant	herbelin
2007-04-29	Quelques exemples sur l'asymétrie de la conversion	herbelin
2007-04-29	Plus d'option -v8 dans coqmktop	herbelin
2007-04-29	Multiples changements autour des implicites :	herbelin
2007-04-29	Suite commit 9810	herbelin
2007-04-29	Ajout possibilité d'options à trois mots.	herbelin
2007-04-29	Correction bug #1507 (report révision 9807 de v8.1 vers trunk)	herbelin
2007-04-28	Correction bug #1519	herbelin
2007-04-28	Ajout de la possibilité de faire référence dans certains cas à un nom	herbelin
2007-04-28	Déplacement des opérations sur bool dans l'état initial	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	Documentation de Existential et de Show Existential (fixes bug #1294)	notin
2007-04-26	Petite modif dans instantiate_pf_com: ajout de test pour l'indice 0, et unifo...	notin
2007-04-26	fin des conclusions multiples	corbinea
2007-04-25	New keyword "Inline" for Parameters and Axioms for automatic	soubiran
2007-04-25	(PR#1529)	soubiran
2007-04-25	Utilisation du nouveau "Unset Elimination Schemes" pour empêcher la création	herbelin
2007-04-24	Le configure et le README accordent leurs violons pour exiger ocaml 3.07 (res...	herbelin
2007-04-24	MAJ ppc/i386	herbelin
2007-04-23	Correction du bug #1496 (ajout de Program Definition et Program Fixpoint aux ...	notin
2007-04-18	Fixed some typos.	glondu
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-17	Corrected a LaTeX typo.	emakarov
2007-04-17	Correct implementation of undo in obligations handling code, correct some bug...	msozeau
2007-04-17	Reorder hook and printing of message, more natural this way.	msozeau