Merge branch 'ralf/as-frac-mode' into 'master'

relax AsFractional Hint Mode

See merge request iris/iris!740

iris/bi/lib/fractional.v

@@ -14,9 +14,10 @@ Global Arguments AsFractional {_} _%I _%I _%Qp.
 
 Global Arguments fractional {_ _ _} _ _.
 
-Global Hint Mode AsFractional - + - - : typeclass_instances.
+Global Hint Mode AsFractional - ! - - : typeclass_instances.
 (* To make [as_fractional_fractional] a useful instance, we have to
-allow [q] to be an evar. *)
+allow [q] to be an evar. The head of [Φ] will always be a λ so ! is
+not a useful mode there. *)
 Global Hint Mode AsFractional - - + - : typeclass_instances.
 
 Section fractional.

tests/heap_lang.v

@@ -368,6 +368,11 @@ Section mapsto_tests.
     iIntros (Φ) "Hl HΦ". Show. wp_load. by iApply "HΦ".
   Qed.
 
+  (* Make sure that we can split a mapsto containing an evar. *)
+  Lemma mapsto_evar_iSplit l v :
+    l ↦{#1 / 2} v -∗  ∃ q, l ↦{#1 / 2 + q} v.
+  Proof. iIntros "H". iExists _. iSplitL; first by iAssumption. Abort.
+
 End mapsto_tests.
 
 Section inv_mapsto_tests.