aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/Record.v
AgeCommit message (Expand)Author
2018-12-19Put #[universes(template)] in outputs testsGaƫtan Gilbert
2017-04-07Better support for printing constructors with let-ins.Hugo Herbelin
2017-04-07Fixing #4499 (not using unnamed record field in {| |} notation).Hugo Herbelin
2011-07-16This adds two option tables 'Printing Record' and 'Printing Constructor'herbelin