fixed formatting

MatteP1 · MatteP1 · commit 50e76469a39d · 2025-09-02T15:21:34.000+02:00
diff --git a/exercises/basics.v b/exercises/basics.v
@@ -129,7 +129,7 @@ Qed.
   entailment [Φ₁ ∗ ... ∗ Φₙ ⊢ Ψ].
 
   Technically, since Iris is built on top of Coq, proving an Iris
-  entailment in Coq corresponds to proving ⊢ₓ (P ⊢ Q). In other
+  entailment in Coq corresponds to proving [⊢ₓ (P ⊢ Q)]. In other
   words, the spatial context is part of the Coq goal. This is the reason
   why the regular Coq tactics no longer suffice. The new tactics work
   with both the non-spatial and the spatial contexts.
diff --git a/theories/basics.v b/theories/basics.v
@@ -129,7 +129,7 @@ Qed.
   entailment [Φ₁ ∗ ... ∗ Φₙ ⊢ Ψ].
 
   Technically, since Iris is built on top of Coq, proving an Iris
-  entailment in Coq corresponds to proving ⊢ₓ (P ⊢ Q). In other
+  entailment in Coq corresponds to proving [⊢ₓ (P ⊢ Q)]. In other
   words, the spatial context is part of the Coq goal. This is the reason
   why the regular Coq tactics no longer suffice. The new tactics work
   with both the non-spatial and the spatial contexts.
