aboutsummaryrefslogtreecommitdiff
path: root/theories/Classes/EquivDec.v
AgeCommit message (Expand)Author
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 18:37:17 +0000