Skip to content

allow specializing a wand with a Coq-level proof of the premise

Ralf Jung requested to merge ralf/into_forall_wand into gen_proofmode

Merge request reports