From 61ac60d40d574b65679eeecc155d21e6f768f690 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 4 Dec 2020 21:39:20 +0100
Subject: [PATCH] Make indentation in proof mode docs consistent.

---
 docs/proof_mode.md | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/docs/proof_mode.md b/docs/proof_mode.md
index 3071750f5..296732ee6 100644
--- a/docs/proof_mode.md
+++ b/docs/proof_mode.md
@@ -248,8 +248,8 @@ Iris
 ----
 
 - `iInv H as (x1 ... xn) "ipat"` : open an invariant in hypothesis H. The result
-   is destructed using the Coq intro patterns `x1 ... xn` (for existential
-   quantifiers) and then the proof mode [introduction pattern][ipat] `ipat`.
+  is destructed using the Coq intro patterns `x1 ... xn` (for existential
+  quantifiers) and then the proof mode [introduction pattern][ipat] `ipat`.
   + `iInv H with "selpat" as (x1 ... xn) "ipat" "Hclose"` : generate an update
   for closing the invariant and put it in a hypothesis named `Hclose`.
   + `iInv H with "selpat" as (x1 ... xn) "ipat"` : supply a selection pattern
-- 
GitLab