aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/typeclasses.mli
Commit message (Expand)AuthorAge
* 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
* Better resolution of implicit parameters in typeclass binders, add extensiona...Gravatar msozeau2008-01-02
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31