Skip to content

Use `<:` (VMcast) for instances of `exact I` in lang/tactics.v

Janno requested to merge ci/janno/vmcast into master

Title says it all. This way we get the benefits of vm_compute both during the proof and at Qed time. It brings the total compilation time down to ~7:40 from ~9:20 on the CI.

/cc @robbertkrebbers

Edited by Janno

Merge request reports