Rudi Grinberg (May 31 2022 at 20:11): Rudi Grinberg (May 31 2022 at 20:11):you could also consider making extraction a separate binary if it would be possible to strip many dependencies from it
Ali Caglayan (May 31 2022 at 20:16):I don't know if it would be possible to separate an extraction binary. The extraction commands are quite complicated: https://coq.inria.fr/refman/addendum/extraction.html
Rudi Grinberg (May 31 2022 at 21:05):Sure, it was just a thought.
Emilio Jesús Gallego Arias (Jun 01 2022 at 12:07):It is possible to make extraction a binary, it should not be hard unless I'm missing something. Similiar to coqnative
Last updated: Jan 30 2023 at 17:03 UTC