aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typeclasses.ml
Commit message (Expand)AuthorAge
* - Fix discharge bug in typeclasses: some constrs were not actuallyGravatar msozeau2009-11-06
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Fixes around typeclasses:Gravatar msozeau2009-10-27
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Remove useless Liboject.export_function fieldGravatar glondu2009-09-17
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Use the proper unification flags in e_exact. This makes exact fail a bitGravatar msozeau2009-07-09
* - Implementation of a new typeclasses eauto procedure based on successGravatar msozeau2009-04-27
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* Correct a bug in commit 11659Gravatar puech2009-01-16
* Fix exponential behaviour of the typeclasses persistent objects. DropGravatar puech2008-12-06
* Fix bug #1943 and restrict the inference optimisation of Program toGravatar msozeau2008-09-15
* Fix bug #1936: uncaught exception due to undefinable exceptions.Gravatar msozeau2008-09-14
* Fix bug #1940: uncaught exception when searching for a type class.Gravatar msozeau2008-09-14
* Fix implementation of "Global Instance" which redeclared the sameGravatar msozeau2008-08-27
* Fix bug in term dnet preventing some unifications. Allow "higher-order"Gravatar msozeau2008-07-28
* Even better test for choosing rewrite or setoid_rewrite.Gravatar msozeau2008-07-26
* Correct implementation of discharging of implicit arguments and add newGravatar msozeau2008-07-22
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
* Various bug fixes in type classes and subtac:Gravatar msozeau2008-07-01
* Code cleanup in typeclasses, remove dead and duplicated code.Gravatar msozeau2008-06-21
* Fix bug in handling of classes and instances inside sections atGravatar msozeau2008-06-17
* Optionally (and by default) split typeclasses evars into connected Gravatar msozeau2008-06-11
* Fixes incorrect handling of existing existentials variables inGravatar msozeau2008-06-03
* Improvements on coqdoc by adding more information into .globGravatar msozeau2008-05-30
* - Fix bug #1858, Hint Unfold calling the wrong locate function.Gravatar msozeau2008-05-23
* Better implementation of the set of instances of a given class as a CmapGravatar msozeau2008-05-15
* Little fixes in setoid_rewrite.Gravatar msozeau2008-04-17
* - Add "Global" modifier for instances inside sections with the usualGravatar msozeau2008-04-15
* Document the new setoid rewrite tactic, and fix a few things whileGravatar msozeau2008-04-12
* Add the ability to specify the implicit status of section variables andGravatar msozeau2008-04-02
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
* Do another pass on the typeclasses code. Correct globalization of classGravatar msozeau2008-03-19
* Add the possibility of specifying constants to unfold for typeclassGravatar msozeau2008-03-17
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
* Change implementation of resolution for typeclasses to use a customizedGravatar msozeau2008-02-08
* New algorithm to resolve morphisms, after discussion with NicolasGravatar msozeau2008-02-06
* Debug 0-ary typeclasses support, use new redefinition support for default tacticGravatar msozeau2008-01-30
* Generalize instance declarations to any context, better name handling. Add ho...Gravatar msozeau2008-01-15
* Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp...Gravatar msozeau2008-01-07
* Fix a naming bug reported by Arnaud Spiwack, allow instance search to create ...Gravatar msozeau2008-01-05
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31