Forked from
Iris / Iris
Source project has a limited visibility.
-
Tej Chajed authored
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.
Tej Chajed authoredThis 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.
