Error on compiling
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"
```
关闭于 2024-01-28 3 条评论