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 unnecessary Absorbing assumption