Not compatible with Coq.8.7

[ildyria]

When trying to compile I get the following error.

git clone git@github.com:math-comp/finmap.git;
cd finmap;
make

which leads to:

File "./finmap.v", line 2309, characters 0-72:
Error:
Ltac call to "by (ssrhintarg)" failed.
Conversion test raised an anomalyAnomaly
                                 "Universe mathcomp.finmap.finmap.1389 undefined."
                                 Please report at http://coq.inria.fr/bugs/.

Admitting the lemma, leads to the following:

File "./finmap.v", line 2444, characters 0-63:
Error:
Ltac call to "by (ssrhintarg)" failed.
Conversion test raised an anomalyAnomaly
                                 "Universe mathcomp.finmap.finmap.1564 undefined."
                                 Please report at http://coq.inria.fr/bugs/.

[CohenCyril]

I worked around the problem. Thanks @ejgallego for repporting to coq/coq.

[CohenCyril]

Actually thanks @matejkosik

[ghost]

@CohenCyril You are welcome.

[strub]

Did you push the workaround? This is still failing here.

[CohenCyril]

Yes I did, what error message do you get?

[strub]

In fact, the opam package is still pointing to:

https://github.com/Barbichu/finmap.git

2017-10-19 19:03 GMT+02:00 Cyril Cohen notifications@github.com:

Yes I did, what error message do you get?

— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or mute the thread.

[CohenCyril]

oops ok :)

[CohenCyril]

Fixed in PR https://github.com/coq/opam-coq-archive/pull/205

[gares]

Hem, @CohenCyril, maybe next time you find a bug in ssr (even if you manage to work around it) tell me ;-)

[maximedenes]

tell me

No, please open an issue on the Coq bug tracker and assign it to Enrico or me.