aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/classes.ml
Commit message (Expand)AuthorAge
* Fix implicit args code so that declarations are added for allGravatar msozeau2009-05-27
* Stop using a "Manual Implicit Arguments" flag and support them as soonGravatar msozeau2009-05-27
* Minor fixes in typeclasses:Gravatar msozeau2009-05-16
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* On remplace evar_map par evar_defs (seul evar_defs est désormais exporté Gravatar aspiwack2009-02-19
* Last changes in type class syntax: Gravatar msozeau2009-01-18
* Correct handling of defined methods (let-ins) in instance declarations.Gravatar msozeau2008-12-04
* More factorization of inductive/record and typeclasses: move classGravatar msozeau2008-11-09
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 01:30:27 +0000