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?

backtracking vs. multi-success extern hints · Issue #4122 · coq/coq
Note: the issue was created automatically with bugzilla2github tool Original bug ID: BZ#4122 From: @jonleivent Reported version: 8.5 CC: @aspiwack

Last updated: Apr 19 2024 at 00:02 UTC