aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/4121.v
AgeCommit message (Expand)Author
2018-10-04rename test files (do not start by a digit)Vincent Laporte
2017-05-17Merge branch 'v8.6'Pierre-Marie Pédrot
2017-05-01remove unneeded -emacs flag to coq-prog-argsPaul Steckler
2017-02-17Moving the Ltac plugin to a pack-based one.Pierre-Marie Pédrot
2015-10-07Univs: add Strict Universe Declaration option (on by default)Matthieu Sozeau
2015-04-09Fix declarations of instances to perform restriction of universeMatthieu Sozeau