coq - The formal proof system

Age	Commit message (Expand)	Author
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
2008-10-27	- Fixed many "Theorem with" bugs.	herbelin
2008-10-26	Correct enormous bug in interpretation of generalized binders: it simply	msozeau
2008-10-26	Fixes and refinements regarding occurrence selection:	herbelin
2008-10-26	adding an option Function_raw_tcc to Function	jforest
2008-10-26	Stop using a coqdocdoc env which prevents use of environments inside	msozeau
2008-10-26	- MAJ svn:ignore pour bin/coq-parser (anciennement bin/parser)	herbelin
2008-10-26	Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui	herbelin
2008-10-25	More debugging of handling of open constrs with typeclasses:	msozeau
2008-10-25	Fix for bug #1981, correct the mismatch between the meta types used in	msozeau
2008-10-24	Raise informative errors instead of Failures or anomalies in case a meta	msozeau
2008-10-24	Fix doc of apply in (see coq-club message 26 September 2008)	herbelin
2008-10-23	Forgot one file which had other local modifications...	msozeau
2008-10-23	Fix bug #1977 by allowing the [apply] variants to take an [open_constr]	msozeau
2008-10-23	Open notation for declaring record instances.	msozeau
2008-10-23	Generalized implementation of generalization.	msozeau
2008-10-22	Fix bugs #1975 and #1976.	msozeau
2008-10-22	Fix for bug #1973 provided by Brian Campbell.	msozeau
2008-10-22	Various coqdoc improvements:	msozeau
2008-10-22	A much better implementation of implicit generalization:	msozeau
2008-10-22	Affichage des notations récursives:	herbelin
2008-10-21	More OCaml-3.11-friendly configure script	glondu
2008-10-21	warning message when a qualid to extract can be both a module or a cst	letouzey
2008-10-21	duplicated open of Ppconstr	letouzey
2008-10-21	Correction bug #1969.	soubiran