Skip to content

Avoid using Hint Resolve with a term

Tej Chajed requested to merge tchajed/stdpp:avoid-constr-hints into master

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.

Merge request reports