Remove coercion status of siProp_valid and uPred_valid

As suggested in iris/iris!358 (merged). Opening as a separate MR because the tests break.

tests/atomic.ref

@@ -30,7 +30,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   heapG0 : heapG Σ
   P : val → iProp Σ
   ============================
-  <<< ∀ x : val, P x >>> code @ ⊤ <<< ∃ y : val, P y, RET #() >>>
+  ⊢ <<< ∀ x : val, P x >>> code @ ⊤ <<< ∃ y : val, P y, RET #() >>>
 1 subgoal
   
   Σ : gFunctors
@@ -62,7 +62,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   heapG0 : heapG Σ
   l : loc
   ============================
-  <<< ∀ x : val, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>
+  ⊢ <<< ∀ x : val, l ↦ x >>> code @ ⊤ <<< l ↦ x, RET #() >>>
 1 subgoal
   
   Σ : gFunctors
@@ -93,7 +93,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   heapG0 : heapG Σ
   l : loc
   ============================
-  <<< l ↦ #() >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
+  ⊢ <<< l ↦ #() >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
 1 subgoal
   
   Σ : gFunctors
@@ -125,7 +125,7 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   heapG0 : heapG Σ
   l : loc
   ============================
-  <<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>
+  ⊢ <<< l ↦ #() >>> code @ ⊤ <<< l ↦ #(), RET #() >>>
 1 subgoal
   
   Σ : gFunctors
@@ -158,7 +158,9 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   heapG0 : heapG Σ
   l : loc
   ============================
-  <<< ∀ x : val, l ↦ x ∗ l ↦ x >>> code @ ⊤ <<< ∃ y : val, l ↦ y, RET #() >>>
+  ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x >>>
+      code @ ⊤
+    <<< ∃ y : val, l ↦ y, RET #() >>>
 1 subgoal
   
   Σ : gFunctors
@@ -177,9 +179,9 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   heapG0 : heapG Σ
   l : loc
   ============================
-  <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
-    code @ ⊤
-  <<< ∃ y : val, l ↦ y, RET #() >>>
+  ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+      code @ ⊤
+    <<< ∃ y : val, l ↦ y, RET #() >>>
 1 subgoal
   
   Σ : gFunctors
@@ -198,10 +200,10 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   heapG0 : heapG Σ
   l : loc
   ============================
-  <<< ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
-    code @ ⊤
-  <<< ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
-      RET #() >>>
+  ⊢ <<< ∀ xx : val, l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+      code @ ⊤
+    <<< ∃ yyyy : val, l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
+        RET #() >>>
 1 subgoal
   
   Σ : gFunctors
@@ -222,9 +224,9 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   heapG0 : heapG Σ
   l : loc
   ============================
-  <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
-    code @ ⊤
-  <<< l ↦ x, RET #() >>>
+  ⊢ <<< ∀ x : val, l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+      code @ ⊤
+    <<< l ↦ x, RET #() >>>
 1 subgoal
   
   Σ : gFunctors
@@ -244,9 +246,9 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   l : loc
   x : val
   ============================
-  <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
-    code @ ⊤
-  <<< ∃ y : val, l ↦ y, RET #() >>>
+  ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+      code @ ⊤
+    <<< ∃ y : val, l ↦ y, RET #() >>>
 1 subgoal
   
   Σ : gFunctors
@@ -267,9 +269,9 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   l : loc
   x : val
   ============================
-  <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
-    code @ ⊤
-  <<< l ↦ #(), RET #() >>>
+  ⊢ <<< l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x ∗ l ↦ x >>>
+      code @ ⊤
+    <<< l ↦ #(), RET #() >>>
 1 subgoal
   
   Σ : gFunctors
@@ -290,9 +292,9 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   l : loc
   xx, yyyy : val
   ============================
-  <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
-    code @ ⊤
-  <<< l ↦ yyyy, RET #() >>>
+  ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+      code @ ⊤
+    <<< l ↦ yyyy, RET #() >>>
 1 subgoal
   
   Σ : gFunctors
@@ -313,10 +315,10 @@ Tactic failure: iAuIntro: not all spatial assumptions are laterable.
   l : loc
   xx, yyyy : val
   ============================
-  <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
-    code @ ⊤
-  <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
-      RET #() >>>
+  ⊢ <<< l ↦ xx ∗ l ↦ xx ∗ l ↦ xx >>>
+      code @ ⊤
+    <<< l ↦ yyyy ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx ∗ l ↦ xx,
+        RET #() >>>
 1 subgoal
   
   Σ : gFunctors