aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Program/Basics.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
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Correct restriction of vm_compute when handling universe polymorphicGravatar Matthieu Sozeau2015-01-15
* Update headers.Gravatar Maxime Dénès2015-01-12
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* 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
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* 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
* Move FunctionalExtensionality to Logic/ (someone please check that theGravatar msozeau2008-12-16
* Remove redefinition of id in Program.Basics, just add maximal implicits.Gravatar msozeau2008-09-13
* Fix setoid_rewrite documentation examples.Gravatar msozeau2008-06-03
* Work on the "occurrences" tactic argument. It is now possible to passGravatar msozeau2008-04-20
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
* Add a flag to control rewriting under lambdas. Otherwise makes someGravatar msozeau2008-03-20
* Reorganize Program and Classes theories. Requiring Setoid no longer setsGravatar msozeau2008-03-16
* Syntax changes in typeclasses, remove "?" for usual implicit argumentsGravatar msozeau2008-03-06
* Proper implicit arguments handling for assumptionsGravatar msozeau2008-02-26
* Debugging of the class_setoid tactic and eauto. Prepare for move fromGravatar msozeau2008-02-13
* New algorithm to resolve morphisms, after discussion with NicolasGravatar msozeau2008-02-06
* Add new files theories/Program/Basics.v and theories/Classes/Relations.vGravatar msozeau2008-02-03