Fix the compilation warnings

[Columbus240]

The newer coq versions give some compilation warnings about how some hints are defined. (fragile-hint-constr)

Look into that and either disable the warning or follow the recommendation of the warning (declare constants for the hints).

[Columbus240]

Fixing the deprecated-ident-entry warnings (from v8.13 upwards) is impossible while staying compatible with v8.10. I propose making a new release of the opam package, then dropping support for v8.10.

The fragile-hint-constr warnings don't look convincing to me for our use-case. Whenever we use it, we declare @some_lemma to be the hint. I see the following options:

• ignore the warning, as we currently did
• silence the warning with Local Set Warnings "-fragile-hint-constr".
• define intermediate values like Local Definition some_lemma' := @some_lemma thus cluttering the namespaces.
• make all arguments of these lemmas explicit (maybe then applying the lemmas will behave differently?)
• verify coqc well-enough, to show that the warning can be removed for hints of this form. Then land an appropriate change.

Has been resolved. A non-issue upon closer inspection.

[Zimmi48]

@Columbus240 Are you sure that these hints would behave differently if you just dropped the @? IINM it used to be the case but it isn't anymore. cc @ppedrot

[ppedrot]

Globals behave the same as their @-explicit form in hints commands at least since Coq 8.5.

[Columbus240]

Hm, I thought I tried that once and it failed. Will check again. Thanks for pointing that out.

[ppedrot]

Note that it's not the case for the using clause of auto tactics, where foo and @foo are not the same thing (see coq/coq#12512 for instance). This might be the source of the confusion.

[Columbus240]

It seems Hint Rewrite can't cope with implicit arguments. But that's probably because Hint Rewrite is something different from Hint Unfold, Hint Resolve, etc.

Lemma foo {X : Type} : 0 = 0.
Admitted.

Lemma bar (X : Type) : 0 = 0.
Admitted.

Fail Hint Rewrite foo : core. (* Cannot infer implicit parameter X of foo whose type is "Type". *)
Hint Rewrite bar : core.

Concretely, the first failure appeared on inverse_image_empty, when I removed the @ in InverseImage.v.

[ppedrot]

Despite the name, Hint Rewrite is a completely different beast that does behave differently on foo and @foo. But it shouldn't complain with a warning if you pass it an arbitrary term (otherwise it's a bug). Just fix the warnings.

[Columbus240]

?
The fragile-hint-constr warnings are on Hint Rewrite @inverse_image_empty : sets.. So you mean its a bug that the warnings appear there?

Edit: In terms of foo:

Lemma foo {X : Type} : 0 = 0.
Admitted.

Hint Rewrite @foo : core. (* causes a 

Edit: I was mistaken, the warnings came from the `Hint Resolve` and not from the `Hint Rewrite`. Sorry.

[Columbus240]

I probably treated the Hint Resolve and the Hint Rewrite warnings the same, and always removed the @ for both kinds of hints (if they were next to eachother in a file), instead of only treating the Hint Resolve.
Thanks for the assistance.