coq - The formal proof system

Age	Commit message (Expand)	Author
2006-10-05	Correction de deux cas où les types inductifs n'étaient pas comparés	herbelin
2006-10-05	revert, the previous commit was a mistake	bertot
2006-10-05	avertissement a propos du commit 9211 dans CHANGES	letouzey
2006-10-05	A version of natprering that should be more efficient and removal of a bad	bertot
2006-10-05	revision de la semantique de rewrite ... in <clause>. details dans la doc	letouzey
2006-10-05	Arith NArith et ZArith exportent ring + nettoyage dans Ring_polynom	barras
2006-10-05	Corrects the problem described in PR#1240:	bertot
2006-10-05	Essai de changement de sémantique du %scope :	herbelin
2006-10-04	Ajout String	herbelin
2006-10-04	inefficacite de field_simplify_eq	barras
2006-10-04	Correction bug #1211	notin
2006-10-04	Correction bug #1204 + maj CHANGES	notin
2006-10-04	Correction bug #1236	notin
2006-10-04	Doc injection as	herbelin
2006-10-03	Changement de comportement du [rewrite ... in H]: Coq échoue si H	notin
2006-10-03	le parsing du LETIN ne suivait pas la DTD (bug #1237)	herbelin
2006-10-03	Retour sur la suppression du pf_nf (trop d'exemples utilisent avec	herbelin
2006-10-03	Détection ocaml 3.09 des variables non utilisées (trop peu pour solliciter ...	herbelin
2006-10-02	nouveau ring/field	barras
2006-10-02	bug dans field_simplify	barras
2006-10-01	Une passe sur l'injection et la discrimination...	herbelin
2006-10-01	Ajout allowed_sorts	herbelin
2006-09-30	Suppression de la comparaison (inutile) des paramètres globaux des	herbelin
2006-09-29	args implicites dans Field	barras
2006-09-29	Added a new option -emacs-U changing emacs prompt delimiters by	courtieu
2006-09-29	Reactivation des outils de developpement de Jacek	herbelin
2006-09-29	Suppression des warnings à la compilation	notin
2006-09-29	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9188 85f007b7-540e-04...	barras
2006-09-28	separation de RealField	barras
2006-09-28	Suppression des lignes vides dans l'affichage des scripts	notin
2006-09-28	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9185 85f007b7-540e-04...	barras
2006-09-28	Add dependent list combinators test.	msozeau
2006-09-28	Makefile : COQLIB -> FULLCOQLIB	corbinea
2006-09-27	Detection des paramettres pour les Functions bien fondees	jforest
2006-09-26	petits pbs de dependances	barras
2006-09-26	Compilation newring	notin
2006-09-26	commit de field + renommages	barras
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	Corrections mineures	notin
2006-09-25	Permet a un unfold de recevoir ses occurences a travers une variable Ltac.	letouzey
2006-09-24	Tentative d'amélioration du message d'erreur en cas de paramètre non laissé	herbelin
2006-09-24	Correction bug dans détection clause "in" mal formée quand le "in" est	herbelin
2006-09-23	Correction d'un bug de coercion de pattern introduit dans la 8.1beta	herbelin
2006-09-23	Correction bug #1168 (dans les coercions de pattern, c'est le nombre	herbelin
2006-09-23	Correction bug #1179 (result of Notation.decompose_notation_key in wrong order	herbelin
2006-09-23	Wish #1187 granted (support for canonical structures that are records	herbelin
2006-09-23	Correction bug #1229 (toplevel "unresolved evar" fled through	herbelin
2006-09-23	Déplacement surround dans util.ml et parenthésage des déclarations	herbelin
2006-09-23	- Correction filtrage des notations impliquant un "match" : la présence	herbelin