gmalecha / coq-ltac-iter

Access hint databases from tactics.
MIT License
12 stars 3 forks source link

Typo in README.md: leftover "run" keyword #4

Closed jeremie-koenig closed 8 years ago

jeremie-koenig commented 8 years ago

Hi Gregory,

The example in README.md still has foreach [ db:my_lemmas ] run k; you may want to drop run.

Best,

jeremie-koenig commented 8 years ago

Also, "combines the invocations of k in the same was a first" -> should read way as.

gmalecha commented 8 years ago

Fixed in d418ff867e8cd0524f17f40f0c94860dc0611984.

In the future, feel free to submit pull-requests.