aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typeclasses.ml
Commit message (Expand)AuthorAge
* 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
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 22:34:55 +0000