Avoid using Hint Resolve with a term

This feature is now deprecated in Coq master (see https://github.com/coq/coq/pull/7791).

Instead of passing a partially-applied lemma directly to Hint Resolve, first create a definition and then make that reference a hint.

Thanks!

Small nit, it's probably better to use coPset_ as a prefix instead of a suffix, since it sort of denotes a "module".

Another one, since we don't really want these lemmas to be used, wouldn't it make sense to use "Local Definition"?

Both of those make sense, done.

added 1 commit

• 747d339b - Avoid using Hint Resolve with a term

Compare with previous version

Yet another nit, I think all A:=positive annotations can be removed. Coq will infer those from the type class constraint on C:=coPset.

(They were probably not needed in the old version either).

Yes, I noticed that but preferred consistency.

+1 for consistency, but consistency with what in this case?

added 1 commit

• 7b5e32b9 - Avoid using Hint Resolve with a term

Compare with previous version

Oh I removed the argument, I just meant I wanted to make minimal changes.

merged

mentioned in commit 3153d46d

Oh, I don't really mind about that TBH.

Thanks and merged!