Got it, thanks!
Arpan Agrawal has marked this topic as resolved.
@Gaëtan Gilbert, I'm still running into issues with this, and I'm getting different error messages on two different opam switches (both using Coq 8.12). This is my _CoqProject file: https://github.com/agrarpan/pumpkin-pi/blob/coq-8.12/plugin/_CoqProject
When I run coqc coq/TestLift.v, I get either "Test not found" or "ornaments.cxms" not found. Could you please tell me what I'm doing wrong?
Last updated: Oct 13 2024 at 01:02 UTC