coq - The formal proof system

Age	Commit message (Expand)	Author
2008-11-14	retour sur le commit 11579 qui faisait plante les contribs FSet et color.	soubiran
2008-11-13	Tentative d'amélioration de la robustesse des Makefile générés par	notin
2008-11-13	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11583 85f007b7-540e-0...	barras
2008-11-12	Correction du bug #1995	notin
2008-11-12	Les signatures des applications de foncteur sont précalculées, cela alourdi...	soubiran
2008-11-10	Makefile.build: an OPTFLAGS behind a bytecode ocamlc (which refuses -p)	letouzey
2008-11-10	Fix mixup between Record, Structure and Class by adding a new variant for	msozeau
2008-11-10	Fix bug reported by Mark Dickinson on Coq-Club about [setoid_rewrite] not	msozeau
2008-11-09	- Correction erreur dans test output Notation.v	herbelin
2008-11-09	f_equal : solve an inefficiency issue (apply vs. simple apply)	letouzey
2008-11-09	better fix for #1931 by using sort_of	letouzey
2008-11-09	Oops... forgot to commit a file related to r11561.	msozeau
2008-11-09	Add test-suite file related to discussion of syntax of implicit binders.	msozeau
2008-11-09	More factorization of inductive/record and typeclasses: move class	msozeau
2008-11-09	- Fixed bug 1968 (inversion failing due to a Not_found bug introduced in	herbelin
2008-11-08	Apply vmconv if there are no _undefined_ evars around.	msozeau
2008-11-07	Slight change of the semantics of user-given casts: they don't really	msozeau
2008-11-07	- Ajout possibilité de lancer ocamldebug sur coqide	herbelin
2008-11-07	Suite #11533	notin
2008-11-07	Correction du bug #1926	notin
2008-11-07	Add some example uses of the new record features in Record.v:	msozeau
2008-11-07	Fix a bug in the specialization by unification tactic related to the problems	msozeau
2008-11-07	Add the ability to give a specific tactic to solve each obligation in	msozeau
2008-11-07	Fix universe problem appearing ConCaT using the existing infrastructure for	msozeau
2008-11-06	Cosmetic: no more whitespace at end of lines in extraction files	letouzey
2008-11-06	Correction d'un petit bug en cas de redéfintion par l'utilisateur de variabl...	notin
2008-11-05	Minor fixes:	msozeau
2008-11-05	Port [rewrite] tactics to open terms. Currently no check that evars	msozeau
2008-11-05	Fix in the unification algorithm using evars: unify types of evar	msozeau
2008-11-05	Move Record desugaring to constrintern and add ability to use notations	msozeau
2008-11-05	Suite commit 11539 sur notation Record dans (Co)Inductive (MAJ	herbelin
2008-11-05	Petit bug dans le commit précédent.	aspiwack
2008-11-05	Nouvelle syntaxe pour écrire des records (co)inductifs :	aspiwack
2008-11-05	Better extraction renaming phase (fix #1914 plus other non-reported bugs)	letouzey
2008-11-04	Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974)	herbelin
2008-11-04	2 petites améliorations de coq_makefile (traitement des .ml4 + cibles géné...	notin
2008-11-02	Fix CAMLHLIB (due to r11358) (Closes: #1986)	glondu
2008-11-02	test-suite/ideal-features/{apply.v -> eapply_evar.v}	glondu
2008-10-31	Ajout d'une option -raw pour Coqdoc (sortie en texte brut)	notin
2008-10-31	allowed patternidents starting with an '_'	amahboub
2008-10-30	The lexer is changer to break former PATTERNIDENT into two tokens.	amahboub
2008-10-29	Document native "Declare ML Module"	glondu
2008-10-29	Remove calls to Dynlink.add_{interfaces,available_units} altogether	glondu
2008-10-29	Adaptation du vieil appel à "apply" sur lemme de symétrie au cas où	herbelin
2008-10-29	Oups...	notin
2008-10-29	Dépendance des cibles de la documentation envers les cibles de Coq	notin
2008-10-28	Native "Declare ML Module" when possible	glondu
2008-10-28	petite modif du commit 11513.	soubiran
2008-10-28	11511 continued (bug in set.out + incohérence dans "Theorem with"	herbelin
2008-10-28	Correction bug 1979.	soubiran