Remove tests mentioning core

tests/proofmode_ascii.v

@@ -15,7 +15,8 @@ Section base_logic_tests.
   Context {M : ucmra}.
   Implicit Types P Q R : uPred M.
 
-  Lemma test_random_stuff (P1 P2 P3 : nat -> uPred M) :
+  (*TODO*)
+  (*Lemma test_random_stuff (P1 P2 P3 : nat -> uPred M) :
     |- forall (x y : nat) a b,
       x ≡ y ->
       <#> (uPred_ownM (a ⋅ b) -*
@@ -38,7 +39,7 @@ Section base_logic_tests.
     iApply ("H3" $! _ 0 with "[$]").
     - iSplit; first done. iApply "H2". iLeft. iApply "H2". by iRight.
     - done.
-  Qed.
+  Qed.*)
 
   Lemma test_iFrame_pure (x y z : M) :
     ✓ x -> ⌜y ≡ z⌝ |-@{uPredI M} ✓ x /\ ✓ x /\ y ≡ z.

tests/proofmode_iris.v

@@ -12,7 +12,8 @@ Section base_logic_tests.
   Context {M : ucmra}.
   Implicit Types P Q R : uPred M.
 
-  Lemma test_random_stuff (P1 P2 P3 : nat → uPred M) :
+  (*TODO*)
+  (*Lemma test_random_stuff (P1 P2 P3 : nat → uPred M) :
     ⊢ ∀ (x y : nat) a b,
       x ≡ y →
       □ (uPred_ownM (a ⋅ b) -∗
@@ -35,7 +36,7 @@ Section base_logic_tests.
     iApply ("H3" $! _ 0 with "[$]").
     - iSplit; first done. iApply "H2". iLeft. iApply "H2". by iRight.
     - done.
-  Qed.
+  Qed.*)
 
   Lemma test_iFrame_pure (x y z : M) :
     ✓ x → ⌜y ≡ z⌝ -∗ (✓ x ∧ ✓ x ∧ y ≡ z : uPred M).