模块分析：coq / extraction

1. 角色定位

• coq/：Coq 标准库/依赖或补充定义（具体内容需按需要进一步细查）
• extraction/：抽取配置与入口

2. 关键文件

• extraction/extraction.v: 抽取配置与入口

3. 作用

• 负责将 Coq 中的算法与证明成果抽取为 OCaml 代码
• 抽取结果与手写 OCaml 代码共同构成可执行的 ccomp