aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/Arguments_renaming.v
AgeCommit message (Expand)Author
2020-08-28When reporting an implicit argument error on a rename argument, use the renam...Hugo Herbelin
2020-08-19Do not refresh the names of implicit arguments.Jasper Hugunin
2020-02-13Arguments: removing the restriction to set an anonymous parameter implicit.Hugo Herbelin
2018-10-04Test-suite: avoid explicit references to “Top”Vincent Laporte
2016-11-07Fix #5182: "Arguments names must be distinct." is bogus and underinformativeMaxime Dénès
2016-10-27Complete overhaul of the Arguments vernacular.Maxime Dénès
2016-09-29Arguments: cleanup + detect discrepancy rename/implicit (#3753)Enrico Tassi
2016-06-29Fix issues in test-suite revealed by warnings.Maxime Dénès
2013-07-29better error message for unexpected renaming (closes #2987)gareuselesinge
2011-12-19Arguments: check rename even if no implicit is specifiedgareuselesinge
2011-12-06Minor fixes to Argumentsgareuselesinge
2011-11-21Renamig support added to "Arguments"gareuselesinge