Cleanup is possible in newer versions of Coq - Githubissues

gmalecha / coq-ltac-iter

Access hint databases from tactics.

MIT License

12 stars 3 forks source link

Cleanup is possible in newer versions of Coq #9

Open JasonGross opened 4 years ago

JasonGross commented 4 years ago

Since https://github.com/coq/coq/pull/8037 (landed in 8.9+beta1), your ltac_apply is available as Tacinterp.Value.apply (https://github.com/coq/coq/blob/1eb5f0504561224affd93717a9fca0e3162dcdd9/plugins/ltac/tacinterp.mli#L31)