coq - The formal proof system

Age	Commit message (Expand)	Author
2009-01-06	Installation des librairies: on utilise maintenant LINKCMO au lieu de	notin
2009-01-05	Completed 11745 (move of jprover to user contribs) and cleaned 11743	herbelin
2009-01-04	Added installation of .cmi files in "make install" target of coq_makefile.	herbelin
2009-01-04	Moved JProver to a user contribution (as was decided a long time ago)	herbelin
2009-01-04	Bug dans commit 11743	herbelin
2009-01-04	Fixed bugs #2001 (search_guard was overwriting the guard index given	herbelin
2009-01-03	Fixed two problems:	herbelin
2009-01-02	Regression test for bug #1967	herbelin
2009-01-02	Conséquence renommage canonique de refl_equal en eq_refl.	herbelin
2009-01-02	Made the debugger work again:	herbelin
2009-01-02	Fixed two apparent inconsistencies in matching.ml:	herbelin
2009-01-02	- Temptative change to notations like "as [\|n H]_eqn" or "as [\|n H]_eqn:H",	herbelin
2009-01-01	Update	herbelin
2009-01-01	Switched to "standardized" names for the properties of eq and	herbelin
2009-01-01	- Fixed bug #2021 (uncaught exception with injection/discriminate when	herbelin
2008-12-31	Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->	herbelin
2008-12-30	- Fixed bugs and compatibilities issues in	herbelin
2008-12-29	- Added support for subterm matching in SearchAbout.	herbelin
2008-12-29	Produce better html code with coqdoc and improve doc:	msozeau
2008-12-29	compatibility with lablgtk2 version 2.12	bertot
2008-12-28	- Another bug in get_sort_family_of (sort-polymorphism of constants and	herbelin
2008-12-26	FMaps: various updates (mostly suggested by P. Casteran)	letouzey
2008-12-26	- Extracted from the tactic "now" an experimental tactic "easy" for small	herbelin
2008-12-26	11715 continued	herbelin
2008-12-26	- Optimized "auto decomp" which had a (presumably) exponential in	herbelin
2008-12-26	- Suppression date dans configure du trunk	herbelin
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