aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* Produce better html code with coqdoc and improve doc:Gravatar msozeau2008-12-29
* compatibility with lablgtk2 version 2.12Gravatar bertot2008-12-29
* - Another bug in get_sort_family_of (sort-polymorphism of constants andGravatar herbelin2008-12-28
* FMaps: various updates (mostly suggested by P. Casteran)Gravatar letouzey2008-12-26
* - Extracted from the tactic "now" an experimental tactic "easy" for smallGravatar herbelin2008-12-26
* 11715 continuedGravatar herbelin2008-12-26
* - Optimized "auto decomp" which had a (presumably) exponential inGravatar herbelin2008-12-26
* - Suppression date dans configure du trunkGravatar herbelin2008-12-26
* - 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 14:16:08 +0000