Open yiyunliu opened 1 year ago
This PR adds #[export] to the coq files in the headers directory. I also made minor tweaks such as Omega -> lia so the code compiles with coq 8.17.
#[export]
Omega -> lia
This PR adds
#[export]
to the coq files in the headers directory. I also made minor tweaks such asOmega -> lia
so the code compiles with coq 8.17.