coq - The formal proof system

Age	Commit message (Expand)	Author
2008-12-24	- coq_makefile: target install now respects the original tree structure	herbelin
2008-12-22	Typo in Makefile leading to empty quote_plugin.cma	letouzey
2008-12-22	FMap: fold_rec + more permissive transpose hyp + various cleanup	letouzey
2008-12-19	Nettoyage des variables Coq et amélioration de coqmktop. Les	notin
2008-12-18	Désactivation de dumpglob lors des appels a functional induction (erreurs pa...	notin
2008-12-18	Maintenant on scan les .ml pour les .dot/.dep.ps (fait avec Matthias).	aspiwack
2008-12-18	Ajout des fichiers de lib/ dans les dépendences générées par make	aspiwack
2008-12-18	Correction d'un bug causant un Not_found dans la contrib FSet.	soubiran
2008-12-18	FSets: integration of suggestions by P. Casteran and S. Lescuyer	letouzey
2008-12-18	- Fixed cutrewrite bug #2021 introduced in commit 11662 (as a side	herbelin
2008-12-17	Avoid printing that extraction has created file Foo when it's not the case	letouzey
2008-12-17	Better compatibility after commit 11693 by adding an alias OrderedTypeFacts.e...	letouzey
2008-12-17	FSet/OrderedType now includes an eq_dec, and hence become an extension of Dec...	letouzey
2008-12-17	Sequel of 11697: repair coqtop.byte when contribs are statically linked (+min...	letouzey
2008-12-16	Extraction Blacklist : a new command for avoiding conflicts with existing files	letouzey
2008-12-16	Extraction: also comply to Set Printing Width when producing external files	letouzey
2008-12-16	Take advantage of natdynlink when available: almost all contribs become loada...	letouzey
2008-12-16	Move FunctionalExtensionality to Logic/ (someone please check that the	msozeau
2008-12-16	Finish fix for the treatment of [inverse] in [setoid_rewrite], making a	msozeau
2008-12-16	Fix for syntax changes in test-suite scripts.	msozeau
2008-12-15	Add some unicode symbols from japanese CJC (request by Y. Regis-Gianas)	letouzey
2008-12-14	Fix looping class resolution bug discovered by B. Aydemir and use the	msozeau
2008-12-14	Fixes in the type classes documentation:	msozeau
2008-12-14	Generalized binding syntax overhaul: only two new binders: `() and `{},	msozeau
2008-12-12	- configure: do not strip coqtop on Darwin so as to support dynamic loading	herbelin
2008-12-12	Uniformity with the rest of the StdLib : _symm --> _sym	letouzey
2008-12-12	Fixed in bug in previous 11662 (incorrect with_evars flag in descend_conjunct...	herbelin
2008-12-11	Structural definition of PositiveMap.fold	glondu
2008-12-11	do not install coqchk cmi files	barras
2008-12-11	Make PositiveMap.xmapi structural	glondu
2008-12-10	Bug in 11662 (did not notice that dp_zenon.mll should be modified instead of	herbelin
2008-12-09	About "apply in":	herbelin
2008-12-08	Fix handling of [inverse] in setoid_rewrite, with an hopefully complete	msozeau
2008-12-06	Fix exponential behaviour of the typeclasses persistent objects. Drop	puech
2008-12-04	Do not catch _all_ exceptions in setoid unification.	msozeau
2008-12-04	Correct handling of defined methods (let-ins) in instance declarations.	msozeau
2008-12-04	Fix priority of the Leibniz Setoid instance to 10 (thanks to M. Lasson	msozeau
2008-12-04	Fixes for unification and substitution of metas under binders.	msozeau
2008-12-03	improved simpl	barras
2008-12-02	Add new directory for pre-compilation of files needed for further tests.	herbelin
2008-12-02	Miscellaneous fixes and improvements:	herbelin
2008-12-02	fixed kernel bug (de Bruijn) + test-suite	barras
2008-11-28	another bug with simpl	barras
2008-11-28	Inductive parameters: nicer doc examples and error message	letouzey
2008-11-27	Test case for previous commit.	msozeau
2008-11-27	Fix (?) a pattern matching compilation problem:	msozeau
2008-11-27	fixed non-exhaustive pattern matching	barras
2008-11-27	fixed bug 1791: simpl was performing eta expansion	barras
2008-11-27	added tests for hyps reordering	barras
2008-11-27	fixing problem with CompCert: reordering resulting from tac change was not cl...	barras