aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/arguments_renaming.ml
Commit message (Expand)AuthorAge
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\
| * Complete overhaul of the Arguments vernacular.Gravatar Maxime Dénès2016-10-27
* | CLEANUP: switching from "right-to-left" to "left-to-right" function compositi...Gravatar Matej Kosik2016-08-30
* | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
* | CLEANUP: removing superfluous (module) qualifiersGravatar Matej Kosik2016-08-24
* | Changing the definition of the "Lib.variable.info" type to enable us to do mo...Gravatar Matej Kosik2016-08-24
|/
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Update headers.Gravatar Maxime Dénès2015-01-12
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* code simplifications concerning SummaryGravatar letouzey2013-04-22
* Fix #3001 (rename arg of global cst inside section)Gravatar gareuselesinge2013-04-18
* Modulification of nameGravatar ppedrot2012-12-18
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Renamig support added to "Arguments"Gravatar gareuselesinge2011-11-21