Stream: Coq users

Topic: Backtracking TC search & `Hint Extern`


view this post on Zulip Janno (Jan 22 2021 at 12:17):

I was reading https://github.com/coq/coq/issues/4122 and I wondered if the issue reflects the current state of affairs: is there really no way to get multi-success behavior from Hint Extern during TC search?

Note: the issue was created automatically with bugzilla2github tool Original bug ID: BZ#4122 From: @jonleivent Reported version: 8.5 CC: @aspiwack

Last updated: Feb 06 2023 at 13:03 UTC