search

gmalecha / coq-ltac-iter

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

avoid anomolies when a hint database doesn't exist #6

Closed gmalecha closed 5 years ago

gmalecha commented 5 years ago

The solution here is to print a warning but treat the database as empty.