aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Program/Subset.v
Commit message (Expand)AuthorAge
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Program: Move ProofIrrelevance to Subset.vGravatar Matthieu Sozeau2016-07-08
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Fix some typos.Gravatar Guillaume Melquiond2015-12-07
* Update headers.Gravatar Maxime Dénès2015-01-12
* Make standard library independent of the names generated byGravatar Hugo Herbelin2014-06-04
* Ltac repeat is in fact already doing progressGravatar letouzey2012-10-01
* Updating headers.Gravatar herbelin2012-08-08
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Final part of moving Program code inside the main code. Adapted add_definitio...Gravatar msozeau2012-03-14
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Move FunctionalExtensionality to Logic/ (someone please check that theGravatar msozeau2008-12-16
* Various fixes:Gravatar msozeau2008-05-15
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
* Minor fixes: Gravatar msozeau2008-04-05
* Removed unneeded tactics from RelationClasses. UseGravatar msozeau2008-03-16
* Debug implementation of dependent induction/dependent destruction and documen...Gravatar msozeau2008-01-31
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-21 19:33:25 +0000