Closed erikmd closed 4 years ago
The issue seems to show up at that Qed line:
https://github.com/coq/bignums/blob/v8.11/BigQ/QMake.v#L613
- File "./BigQ/QMake.v", line 613, characters 1-5:
- Error: Anomaly "the kernel does not support existential variables."
- Please report at http://coq.inria.fr/bugs/.
This is just that the 8.11 branch got broken, c.f. https://github.com/coq/coq/issues/11161
Should be solved now.
Thanks @ejgallego !
Cc @palmskog @ejgallego @vbgl FYI
Since last night, the build of
coqorg/coq:8.11-alpha
with coq-bignums.8.11.dev (based on coq_makefile) fails:Do you think this error is expected?
Anyway as suggested in https://github.com/coq/bignums/issues/26#issuecomment-555689676, we could now replace coq_makefile with dune for the coq-bignums.dev extra-dev opam file…