aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/Extraction_matchs_2413.v
AgeCommit message (Expand)Author
2019-08-26Make kernel parametric on the lowest universe and fix #9294Matthieu Sozeau
2018-12-19Put #[universes(template)] in outputs testsGaƫtan Gilbert
2017-06-14Prelude : no more autoload of plugins extraction and recdefPierre Letouzey
2013-01-18Unset Asymmetric Patternspboutill
2010-12-21Extraction: avoid type-unsafe optimisation of pattern-matchings (fix #2413)letouzey