An error occurred while fetching the assigned milestone of the selected merge_request.
Fix issue reported by @jung in https://mattermost.mpi-sws.org/iris/pl/dqsc96ndbinfbyi8m4iuptjchw. Fixes #160 (closed).
The problem is that Hint Immediate translates to (something like) simple apply @finite.finite_countable ; trivial in the trace, and one (or both) the tactics trigger https://github.com/coq/coq/issues/6583. So I've adapted Iris's work around; I've not confirmed whether all of it is needed, but it worked on first try.
Missing (I assume):
trivial only uses hints with cost 0, but typeclasses eauto 0 does not appear to work, so typeclasses eauto 1 is the closest thing I see. This might be a problem.Also see Coq issue https://github.com/coq/coq/issues/16893.