aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/subtac/subtac_classes.ml
Commit message (Expand)AuthorAge
* 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
* Generalized implementation of generalization.Gravatar msozeau2008-10-23
* 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
* Give back progress information after feeding the Program Instance to theGravatar msozeau2008-08-26
* Various bug fixes in type classes and subtac:Gravatar msozeau2008-07-01
* 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
* 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
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* 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
* 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
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
* Proper implicit arguments handling for assumptionsGravatar msozeau2008-02-26
* Backport Program Instance into Instance. Proper early error message ifGravatar msozeau2008-02-10
* Change implementation of resolution for typeclasses to use a customizedGravatar msozeau2008-02-08
* Work on dependent induction tactic and friends, finish the test-suite exampleGravatar msozeau2008-01-30
* 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
* Fix name capture bug and call the right pretyper in subtac.Gravatar msozeau2007-12-31
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31