aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_4836.v
AgeCommit message (Expand)Author
2021-02-26[coqc] Don't allow to pass more than one file to coqcEmilio Jesus Gallego Arias
2019-01-30[toplevel] Deprecate the `-compile` flag in favor of `coqc`.Emilio Jesus Gallego Arias
2016-09-11Add a test for 4836Jason Gross