aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_4132.v
AgeCommit message (Collapse)Author
2021-04-02Remove the omega tactic and related optionsJim Fehrle
2018-10-15Correct some spelling errorsBenjamin Barenblat
Lintian found some spelling errors in the Debian packaging for coq. Fix them most places they appear in the current source. (Don't change documentation anchor names, as that would invalidate external deeplinks.) This also fixes a bug in coqdoc: prior to this commit, coqdoc would highlight `instanciate` but not `instantiate`.
2018-10-04rename test files (do not start by a digit)Vincent Laporte