update to Coq 8.18

Let's see if we get any warnings.

theories/lang/heap.v

@@ -91,7 +91,7 @@ Section to_heap.
   Implicit Types σ : state.
 
   Lemma to_heap_valid σ : ✓ to_heap σ.
-  Proof. intros l. rewrite lookup_fmap. case (σ !! l)=> [[[|n] v]|] //=. Qed.
+  Proof. intros l. rewrite lookup_fmap. destruct (σ !! l) as [[[|n] v]|] eqn:EQ; rewrite EQ //. Qed.
 
   Lemma lookup_to_heap_None σ l : σ !! l = None → to_heap σ !! l = None.
   Proof. by rewrite /to_heap lookup_fmap=> ->. Qed.