aboutsummaryrefslogtreecommitdiff
path: root/theories/Classes/SetoidDec.v
AgeCommit message (Expand)Author
2021-03-30Remove the :> type castJim Fehrle
2021-01-08Modify Classes/SetoidDec.v to compile with -mangle-namesJasper Hugunin
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-05-23Fixing typos - Part 3JPR
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2012-08-08Updating headers.herbelin
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
2012-03-14Final part of moving Program code inside the main code. Adapted add_definitio...msozeau
2011-09-06Avoid registering λ and Π as keywords just for some private Local Notationletouzey
2010-07-31Fixed commit r13359 which was incomplete for its "trunk" part. Thanksherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
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