aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/classes.ml
Commit message (Expand)AuthorAge
...
* Promote evar_defs to evar_map (in Evd)Gravatar glondu2009-11-11
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.Gravatar gmelquio2009-11-04
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Fix bug #2162 and a name clashing bug in generalized binders.Gravatar msozeau2009-10-09
* Correctly do backtracking during type class resolution even if only newGravatar msozeau2009-10-05
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Backtrack on the forced discharge of type class variables introducedGravatar msozeau2009-09-14
* Jolification : tentative de supprimer les "( evd)" et associés quiGravatar aspiwack2009-07-07
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-06 06:39:02 +0000