aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes/SetoidTactics.v
Commit message (Expand)AuthorAge
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
* Rename obligations_tactic to obligation_tactic and fix bugs #1893.Gravatar msozeau2008-06-22
* - Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used toGravatar msozeau2008-05-12
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
* Work on the "occurrences" tactic argument. It is now possible to passGravatar msozeau2008-04-20
* Document CHANGES in setoid rewrite, move DefaultRelation toGravatar msozeau2008-04-15
* Document the new setoid rewrite tactic, and fix a few things whileGravatar msozeau2008-04-12
* - A little cleanup in Classes/*. Separate standard morphisms onGravatar msozeau2008-04-08
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
* Compatibility fixes, backtrack on definitions of reflexive,Gravatar msozeau2008-03-22
* Do another pass on the typeclasses code. Correct globalization of classGravatar msozeau2008-03-19
* Reorganize Program and Classes theories. Requiring Setoid no longer setsGravatar msozeau2008-03-16
* 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
* Proper implicit arguments handling for assumptionsGravatar msozeau2008-02-26
* 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
* 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
* Fix a naming bug reported by Arnaud Spiwack, allow instance search to create ...Gravatar msozeau2008-01-05
* 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