aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/classes.ml
Commit message (Expand)AuthorAge
* Petit bug dans le commit précédent.Gravatar aspiwack2008-11-05
* Nouvelle syntaxe pour écrire des records (co)inductifs :Gravatar aspiwack2008-11-05
* Open notation for declaring record instances.Gravatar msozeau2008-10-23
* Generalized implementation of generalization.Gravatar msozeau2008-10-23
* Fix bugs #1975 and #1976.Gravatar msozeau2008-10-22
* Fix bug #1943 and restrict the inference optimisation of Program toGravatar msozeau2008-09-15
* In manual implicit arguments mode, do not enrich implicitsGravatar msozeau2008-09-14
* 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
* Add enough information to correctly globalize recursive calls in inductive andGravatar msozeau2008-09-11
* Fixes in typeclasses resolution. Avoid reducing instances types beforeGravatar msozeau2008-09-07
* - New auto hints for transparency/opacity control, not bound to Gravatar msozeau2008-08-22
* Correct implementation of discharging of implicit arguments and add newGravatar msozeau2008-07-22
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* - Improve [Context] vernacular to allow arbitrary binders, not justGravatar msozeau2008-07-07
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
* Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...Gravatar notin2008-06-25
* 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
* Fix bug in implementation of splitting of class constraints.Gravatar msozeau2008-06-18
* Fix bug in handling of classes and instances inside sections atGravatar msozeau2008-06-17
* Fixes w.r.t. let binders in class contexts and Add ParametricGravatar msozeau2008-06-17
* 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
* Fix globalization bug in class_tactics and refactorize instanceGravatar msozeau2008-05-19
* - Add "Global" modifier for instances inside sections with the usualGravatar msozeau2008-04-15
* Add the ability to specify what to do with free variables in instanceGravatar msozeau2008-04-12
* Check that no evars remain in instance types earlier at InstanceGravatar msozeau2008-04-11
* - A little cleanup in Classes/*. Separate standard morphisms onGravatar msozeau2008-04-08
* 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
* Various fixes on typeclasses:Gravatar msozeau2008-03-27
* Fix a bug found by B. Grégoire when declaring morphisms in moduleGravatar msozeau2008-03-23
* Do another pass on the typeclasses code. Correct globalization of classGravatar msozeau2008-03-19
* Do a second pass on the treatment of user-given implicit arguments. NowGravatar msozeau2008-03-15
* Fix bugs that were reopened due to the change of setoidGravatar msozeau2008-03-08
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
* New instance returns the (future) identifier of the instance.Gravatar msozeau2008-02-26
* Proper implicit arguments handling for assumptionsGravatar msozeau2008-02-26
* Backport Program Instance into Instance. Proper early error message ifGravatar msozeau2008-02-10
* Fix the clrewrite tactic, change Relations.v to work on relations in PropGravatar msozeau2008-02-09
* 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
* Change notation for setoid inequality, coerce objects before comparing them. ...Gravatar msozeau2008-01-18
* 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
* Implicit arguments in class field declarationsGravatar msozeau2008-01-02
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31