Stream: Coq users

Topic: Backtracking TC search & `Hint Extern`

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

I was reading 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: Jun 24 2024 at 14:01 UTC