aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/3612.v
AgeCommit message (Expand)Author
2018-10-04rename test files (do not start by a digit)Vincent Laporte
2017-06-15plugins/ltac : avoid spurious .cmxs filesPierre Letouzey
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
2016-04-04Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...Matthieu Sozeau
2016-02-29Moving the "clear" tactic to TACTIC EXTEND.Pierre-Marie Pédrot
2015-08-14Move type_scope into user space, fix some output logsJason Gross
2015-02-27Adding a test for bug #3612.Pierre-Marie Pédrot