aboutsummaryrefslogtreecommitdiff
path: root/pretyping/arguments_renaming.ml
AgeCommit message (Expand)Author
2016-10-27Complete overhaul of the Arguments vernacular.Maxime Dénès
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-08-03Move to a representation of universe polymorphic constants using indices for ...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-04-22code simplifications concerning Summaryletouzey
2013-04-18Fix #3001 (rename arg of global cst inside section)gareuselesinge
2012-12-18Modulification of nameppedrot
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-03-02Noise for nothingpboutill
2011-11-21Renamig support added to "Arguments"gareuselesinge