aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Classes/EquivDec.v
Commit message (Expand)AuthorAge
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Updating headers.Gravatar herbelin2012-08-08
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
* Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).Gravatar herbelin2012-04-15
* Final part of moving Program code inside the main code. Adapted add_definitio...Gravatar msozeau2012-03-14
* Everything compiles again.Gravatar msozeau2012-03-14
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Remove various useless {struct} annotationsGravatar letouzey2009-11-02
* Add a new vernacular command for controling implicit generalization ofGravatar msozeau2009-10-27
* Fix the stdlib doc compilation + switch all .v file to utf8Gravatar letouzey2009-09-28
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Fix compilation errors due to last commit.Gravatar msozeau2009-09-15
* Stop using a "Manual Implicit Arguments" flag and support them as soonGravatar msozeau2009-05-27
* Just export RelationClasses for [Equivalence] through Setoid.Gravatar msozeau2009-04-18
* Rewrite of Program Fixpoint to overcome the previous limitations: Gravatar msozeau2009-03-28
* Last changes in type class syntax: Gravatar msozeau2009-01-18
* Move FunctionalExtensionality to Logic/ (someone please check that theGravatar msozeau2008-12-16
* Generalized binding syntax overhaul: only two new binders: `() and `{},Gravatar msozeau2008-12-14
* Rename obligations_tactic to obligation_tactic and fix bugs #1893.Gravatar msozeau2008-06-22
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
* Postpone the search for the recursive argument index from the user givenGravatar msozeau2008-05-06
* Fix the last compilation problemGravatar msozeau2008-04-09
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
* - Second pass on implementation of let pattern. Parse "let ' par [as x]?Gravatar msozeau2008-03-28
* Various fixes on typeclasses:Gravatar msozeau2008-03-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 14:30:28 +0000