Need Coq.Program.Tactics.

[corwin-of-amber]

In Coq 8.14 (rc1), I am getting this:

File "./finmap/finmap.v", line 752, characters 0-186:
Error: Library Coq.Program.Tactics has to be required first.

Indeed adding Require Coq.Program.Tactics. at the beginning of finmap.v solves the problem.

[ejgallego]

@corwin-of-amber are you using the fast-load patch?

One of the effects the patch has is to remove that implicit import. I agree that it would be nice to make this dependency on Program explicit [IIRC it is due rewriting with the setoid for iff]

Please annoy me so upstream that fast-load patch for once and for all.

[corwin-of-amber]

Oh yes! I completely forgot about that patch.

So that import comes from somewhere within (core) mathcomp I guess. Agreed, it should be here as well, anyway.

[ejgallego]

So that import comes from somewhere within (core) mathcomp I guess. Agreed, it should be here as well, anyway.

It comes from a side effect of importing (non used) Coq arithmetic libs. That used to weight 100MiB so hence the reason I implemented that optimization. Will try to upstream that soon, sorry for the lag on this.