aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes
Commit message (Expand)AuthorAge
...
* Proper implicit arguments handling for assumptionsGravatar msozeau2008-02-26
* Backtrack changes on eauto, move specialized version of eauto inGravatar msozeau2008-02-14
* Debugging of the class_setoid tactic and eauto. Prepare for move fromGravatar msozeau2008-02-13
* 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
* Fix obligations not being discharged due to new definition of complement.Gravatar msozeau2008-02-06
* New algorithm to resolve morphisms, after discussion with NicolasGravatar msozeau2008-02-06
* Add new files theories/Program/Basics.v and theories/Classes/Relations.vGravatar msozeau2008-02-03
* Debug implementation of dependent induction/dependent destruction and documen...Gravatar msozeau2008-01-31
* Support for occurences and 'in' in class_setoid, work on corresponding tactic...Gravatar msozeau2008-01-30
* Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ...Gravatar msozeau2008-01-18
* Change notation for setoid inequality, coerce objects before comparing them. ...Gravatar msozeau2008-01-18
* Fix Makefile bug, using .v instead of .vo and document SetoidDec.vGravatar msozeau2008-01-17
* Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...Gravatar msozeau2008-01-17
* 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
* Remove spurious .d, better tactics.Gravatar msozeau2008-01-07
* Fix a naming bug reported by Arnaud Spiwack, allow instance search to create ...Gravatar msozeau2008-01-05
* Add partial setoids in theories/Classes, add SetoidDec class for setoids with...Gravatar msozeau2008-01-04
* Move Classes.Setoid to Classes.SetoidClass to avoid name clash.Gravatar msozeau2007-12-31
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31