aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/5036.v
AgeCommit message (Collapse)Author
2018-10-04rename test files (do not start by a digit)Vincent Laporte
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2016-09-29Fix bug #5036 autorewrite, sections and universesMatthieu Sozeau
Universe context not properly declared. Improve API and code in declare.ml to allow declaration of universe contexts, used by declaration of universes and constraints (separately).