Extraction problem with Coq-8.11
Flocq have name collision with standard library which prevents extraction from working:
"coqtop" -q -w none -R coq Vellvm -R ml/extracted Extract -R ../lib/InteractionTrees/theories/ ITree -batch -load-vernac-source ml/extracted/Extract.v
File "/home/lord/coq/vellvm/src/ml/extracted/Extract.v", line 48, characters 0-38:
Error:
The Coq modules Coq.Floats.SpecFloat and Flocq.IEEE754.SpecFloat.SpecFloat have the same ML name.
This is not supported yet. Please do some renaming first.
The problem first manifested after upgrade to coq-flocq-3.3.0.