coq - 关于 evas、e* 策略、上下文的 Coq 教程？

Question

我一直在努力寻找关于 Coq Contexts、evars、e* 策略等的好的指南/阅读/练习集。

理想情况下，我想构建一个包含一些抽象变量的 Coq 上下文，稍后我将在 OCaml 或 Haskell 提取中填写这些内容。这可能吗？阅读有关定理漏洞以及如何在 Coq 证明中填充它们的最佳位置是什么？