aboutsummaryrefslogtreecommitdiff
path: root/theories/Classes/EquivDec.v
AgeCommit message (Expand)Author
2021-03-30Remove the :> type castJim Fehrle
2021-01-08Modify Classes/EquivDec.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
2019-05-21Remove undocumented Instance : ! syntaxGaëtan Gilbert
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-04-15Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).herbelin
2012-03-14Final part of moving Program code inside the main code. Adapted add_definitio...msozeau
2012-03-14Everything compiles again.msozeau
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-11-02Remove various useless {struct} 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-09-15Fix compilation errors due to last commit.msozeau
2009-05-27Stop using a "Manual Implicit Arguments" flag and support them as soonmsozeau
2009-04-18Just export RelationClasses for [Equivalence] through Setoid.msozeau
2009-03-28Rewrite of Program Fixpoint to overcome the previous limitations: msozeau
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-06-22Rename obligations_tactic to obligation_tactic and fix bugs #1893.msozeau
2008-05-11- Cleanup parsing of binders, reducing to a single production for allmsozeau
2008-05-06Postpone the search for the recursive argument index from the user givenmsozeau
2008-04-09Fix the last compilation problemmsozeau
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