aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/4533.v
Commit message (Collapse)AuthorAge
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-05-17
|\
| * remove unneeded -emacs flag to coq-prog-argsGravatar Paul Steckler2017-05-01
| |
* | Moving the Ltac plugin to a pack-based one.Gravatar Pierre-Marie Pédrot2017-02-17
|/ | | | | | | This is cumbersome, because now code may fail at link time if it's not referring to the correct module name. Therefore, one has to add corresponding open statements a the top of every file depending on a Ltac module. This includes seemingly unrelated files that use EXTEND statements.
* Fix test-suite file coq-prog-argsGravatar Matthieu Sozeau2016-03-09
| | | | They were not parsed correctly with a newline in the middle.
* Fixed bug #4533 with previous Keyed Unification commitGravatar Matthieu Sozeau2016-03-09
Add test-suite file to ensure non-regression.