aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typeclasses.mli
Commit message (Expand)AuthorAge
* Fix interface of resolve_typeclasses: onlyargs -> with_goals:Gravatar msozeau2012-03-20
* Fix bugs related to Program integration.Gravatar msozeau2012-03-19
* Noise for nothingGravatar pboutill2012-03-02
* Fix for Program Instance not separately checking the resolution of evars of t...Gravatar msozeau2012-01-23
* Restore backward compatibility. ":>" declares subinstances in Class declarati...Gravatar msozeau2011-11-18
* Merge subinstances branch by me and Tom Prince.Gravatar msozeau2011-11-17
* Fix bug #2557 and an issue with Propers for complementGravatar msozeau2011-10-07
* - Make typeclass transparency information directly availableGravatar 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
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Fix the bug-ridden code used to choose leibniz or generalizedGravatar msozeau2009-09-08
* Use the proper unification flags in e_exact. This makes exact fail a bitGravatar msozeau2009-07-09
* Fix exponential behaviour of the typeclasses persistent objects. DropGravatar puech2008-12-06
* Fix in the unification algorithm using evars: unify types of evarGravatar msozeau2008-11-05
* Open notation for declaring record instances.Gravatar msozeau2008-10-23
* 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 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
* 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 #1889, correct globalization in class declarations.Gravatar msozeau2008-06-21
* 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
* Little fixes in setoid_rewrite.Gravatar msozeau2008-04-17
* - Add "Global" modifier for instances inside sections with the usualGravatar msozeau2008-04-15
* 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
* 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