Make `FromPure` depend on an affinity parameter
In a linear logic, a pure premise usually appear under an affinely
modality.
That is, an hypothesis could probably look like bi_affinely ⌜φ⌝ -∗ P
. However, the [%]
specialization pattern will not allow to discharge this premise. The solution is to make FromPure
depend on an affinity Boolean.
In the way, I fixed two bugs in the proofmode:
-
tac_assert_pure
was no longer working. The corresponding Ltac code did not have the right number of parameters -
into_forall_wand_pure
had an unnecessaryAbsorbing
assumption