aboutsummaryrefslogtreecommitdiff
path: root/theories/Classes/SetoidDec.v
AgeCommit message (Expand)Author
2009-10-27Add a new vernacular command for controling implicit generalization ofmsozeau
2009-09-28Fix the stdlib doc compilation + switch all .v file to utf8letouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-01-18Last changes in type class syntax: msozeau
2008-12-16Move FunctionalExtensionality to Logic/ (someone please check that themsozeau
2008-12-14Generalized binding syntax overhaul: only two new binders: `() and `{},msozeau
2008-12-04Fix priority of the Leibniz Setoid instance to 10 (thanks to M. Lassonmsozeau
2008-11-09More factorization of inductive/record and typeclasses: move classmsozeau
2008-07-07- Improve [Context] vernacular to allow arbitrary binders, not justmsozeau
2008-07-04Fixes in handling of implicit arguments:msozeau
2008-05-11- Cleanup parsing of binders, reducing to a single production for allmsozeau
2008-04-01Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientherbelin
2008-03-28- Second pass on implementation of let pattern. Parse "let ' par [as x]?msozeau
2008-03-27Various fixes on typeclasses:msozeau
2008-03-23Fix a bug found by B. Grégoire when declaring morphisms in modulemsozeau
2008-03-08Fix bugs that were reopened due to the change of setoidmsozeau
2008-03-06Syntax changes in typeclasses, remove "?" for usual implicit argumentsmsozeau
2008-02-06Fix obligations not being discharged due to new definition of complement.msozeau
2008-02-03Add new files theories/Program/Basics.v and theories/Classes/Relations.vmsozeau
2008-01-30Support for occurences and 'in' in class_setoid, work on corresponding tactic...msozeau
2008-01-18Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ...msozeau
2008-01-18Change notation for setoid inequality, coerce objects before comparing them. ...msozeau
2008-01-17Fix Makefile bug, using .v instead of .vo and document SetoidDec.vmsozeau
2008-01-07Remove spurious .d, better tactics.msozeau
2008-01-04Add partial setoids in theories/Classes, add SetoidDec class for setoids with...msozeau