From 9117e139d6aad064756f58427ec137d8bb787fcc Mon Sep 17 00:00:00 2001
From: Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr>
Date: Mon, 16 Nov 2020 16:40:22 +0100
Subject: minor fix in coq2html comment

---
 backend/Tunneling.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'backend')

diff --git a/backend/Tunneling.v b/backend/Tunneling.v
index bb1ac9f5..269ebb6f 100644
--- a/backend/Tunneling.v
+++ b/backend/Tunneling.v
@@ -54,7 +54,8 @@ Naively, we may define [branch_t f pc] as follows:
      L1: nop L1;
 >>
   or
-<<   L1: nop L2;
+<<
+     L1: nop L2;
      L2: nop L1;
 >>
   Coq warns us of this fact by not accepting the definition
-- 
cgit