aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typeclasses.ml
Commit message (Expand)AuthorAge
* - Make typeclass transparency information directly availableGravatar msozeau2011-04-13
* - Do not make constants with an assigned type polymorphic (wrong unfoldings).Gravatar msozeau2011-04-13
* - Add modulo_delta_types flag for unification to allow fullGravatar msozeau2011-03-13
* Keep information on which fields are subclasses in class declarations,Gravatar msozeau2011-03-11
* - Fix treatment of globality flag for typeclass instance hints (theyGravatar msozeau2011-02-14
* Misc improvements about evar_mapGravatar letouzey2010-12-15
* Fix bug #2321, allowing "_" named projections in classes. Not realizingGravatar msozeau2010-09-28
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove compile-command pragmas for emacsGravatar letouzey2010-05-19
* Improved the efficiency of evars traverals thanks to a split ofGravatar herbelin2010-05-13
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Compute the correct generalization information when discharging a classGravatar msozeau2010-02-16
* Fix [Existing Class] impl and add documentation. Fix computation of theGravatar msozeau2010-02-10
* Added module sharing support for typeclasses and hints (pri_auto_tactic).Gravatar soubiran2010-01-12
* Fix handling of instance declarations in presence of let-ins (bugGravatar msozeau2010-01-01
* Fix type class discharge again.Gravatar msozeau2009-11-15
* - 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-30 13:50:01 +0000