Mentions légales du service

Skip to content

Add `Require Extraction` to Coq output

The .v file generated by Menhir contains Extract directives, which are no longer accepted if the Extraction standard library module has not been loaded before. Currently, there's an indirect dependency MenhirLib -> FSetAVL -> MSetAVL -> FunInd -> Extraction, but this is about to change, so better be explicit.

Refs: https://github.com/AbsInt/CompCert/pull/515 https://github.com/coq/coq/pull/19343

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information