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