Add tests.

tests/proofmode_iris.ref

@@ -172,6 +172,38 @@ Tactic failure: iInv: invariant "H2" not found.
      : string
 The command has indeed failed with message:
 Tactic failure: iMod: "H" not fresh.
+"test_iIntros_lc"
+     : string
+1 goal
+  
+  Σ : gFunctors
+  invGS0 : invGS Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  n, m : nat
+  ============================
+  "Hlc1" : £ (S n)
+  "Hlc2" : £ m
+  --------------------------------------∗
+  £ (S n)
+"lc_iSplit_lc"
+     : string
+2 goals
+  
+  Σ : gFunctors
+  invGS0 : invGS Σ
+  cinvG0 : cinvG Σ
+  na_invG0 : na_invG Σ
+  n, m : nat
+  ============================
+  "Hlc1" : £ (S n)
+  --------------------------------------∗
+  £ (S n)
+
+goal 2 is:
+ "Hlc2" : £ m
+ --------------------------------------∗
+ £ m
 "test_iInv"
      : string
 1 goal

tests/proofmode_iris.v

@@ -250,6 +250,15 @@ Section iris_tests.
     iIntros "H H'". Fail iDestruct "H'" as ">H".
   Abort.
 
+  (** Make sure that the splitting rule for [+] gets priority over the one for
+  [S]. See issue #470. *)
+  Check "test_iIntros_lc".
+  Lemma test_iIntros_lc n m : £ (S n + m) -∗ £ (S n).
+  Proof. iIntros "[Hlc1 Hlc2]". Show. iExact "Hlc1". Qed.
+
+  Check "lc_iSplit_lc".
+  Lemma lc_iSplit_lc n m : £ (S n) -∗ £ m -∗ £ (S n + m).
+  Proof. iIntros "Hlc1 Hlc2". iSplitL "Hlc1". Show. all: done. Qed.
 End iris_tests.
 
 Section monpred_tests.