Error on compiling

[mizlan]

Coq 8.18, OCaml 4.10.2

when running make -C proofs

COQC List.v
File "./List.v", line 163, characters 0-374:
Error:
Unable to satisfy the following constraints:
In environment:
merge : forall A : Type, (A -> A -> Z) -> list A -> list A -> list A
A : Type
cmp : A -> A -> Z
l1, l3 : list A
merge_aux : list A -> list A
l2, l, l0 : list A
h1 : A
t1 : list A
h2 : A
t2 : list A

?H : "StrictOrder ?R"

?H0 : "OrderDec ?H"

[mizlan]

It seems Z_le_dec works in place of Stdlib.le in the merge function in proofs/List.v

[clarus]

OK thanks for the report! I am able to reproduce the bug, looking for a fix.

[clarus]

The issue should now be fixed on the master branch thanks to #230 !